VERS5 
NIL 
((EPSILONDEF SETS#4) (SET_EXTENSIONALITY SETS#5) (CHOICE SETS#9) (DEMORGAN NORMAL#5) (DEMORGAN1 NORMAL#6) (EXCLUDED_MIDDLE NORMAL#7) (TRANS_COND NORMAL#8) (DISJUNCT_SUBST NORMAL#9) (INCONSISTENT NORMAL#10) (ZERO_NOT_SUCCESSOR NATNUM#6) (SUCCESSOREQ NATNUM#7) (PROOF_BY_INDUCTION NATNUM#8) (LANDAU_TH1 NATNUM#9) (LANDAU_TH2 NATNUM#10) (LANDAU_TH3 NATNUM#11) (LANDAU_TH4 NATNUM#15) (COMMUTADD NATNUM#17) (LANDAU_TH7 NATNUM#18) (LANDAU_TH8 NATNUM#19) (TRCT0 NATNUM#20) (TRCT1 NATNUM#21) (TRCT2 NATNUM#22) (TRCT3 NATNUM#23) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (LANDAU_DEF2 ORDERING#3) (TOTALORD ORDERING#5) (STRICT1 ORDERING#6) (STRICT2 ORDERING#7) (STRICT3 ORDERING#8) (GREATERP_LESSP ORDERING#9) (GRTEQP_LSSEQP ORDERING#14) (TRANSITIVITY_OF_ORDER ORDERING#15) (TRANSITIVITY_OF_GREATERP ORDERING#16) (LSSEQP_LESSP_LESSP ORDERING#17) (LESSP_LSSEQP_LESSP ORDERING#18) (TRANSITIVITY_OF_LSSEQP ORDERING#19) (INCREASING ORDERING#20) (SUCCESSORLESS ORDERING#21) (RPLUS_GREATCAN ORDERING#22) (RPLUS_LESSCAN ORDERING#23) (LANDAU_TH21 ORDERING#24) (LANDAU_A_TH22 ORDERING#25) (LANDAU_B_TH22 ORDERING#26) (LANDAU_TH23 ORDERING#27) (LANDAU_A_TH24 ORDERING#28) (ZEROLEAST1 ORDERING#29) (ZEROLEAST2 ORDERING#30) (LANDAU_B_TH24 ORDERING#31) (LANDAU_TH25 ORDERING#32) (LANDAU_TH26 ORDERING#33) (LANDAU_TH27 ORDERING#34) (LANDAU_DEF6 MULTIP#2) (TIMSUCC MULTIP#5) (LTIMESCAN MULTIP#6) (RTIMESCAN MULTIP#7) (COMMUTMULT MULTIP#8) (LTIMESTOZERO MULTIP#9) (RTIMESTOZERO MULTIP#10) (NOZERODIVISORS MULTIP#11) (TIMESFACT MULTIP#11) (LDISTRIB MULTIP#12) (RDISTRIB MULTIP#13) (LANDAU_A_TH32 MULTIP#14) (LANDAU_D_TH32 MULTIP#15) (LANDAU_A_TH33 MULTIP#16) (LANDAU_B_TH33 MULTIP#17) (LANDAU_C_TH33 MULTIP#18) (LANDAU_TH34 MULTIP#19) (LANDAU_A_TH35 MULTIP#20) (LANDAU_B_TH35 MULTIP#21) (LANDAU_TH36 MULTIP#22) (ALLDEF ALL#3) (SOMEDEF ALL#4) (ALLFACT ALL#5) (SOMEFACT ALL#6) (LISTINDUCTION LISPAX#30) (LISTINDUCTIONDEF LISPAX#34) (SEXPINDUCTION LISPAX#35) (SEXPINDUCTIONDEF LISPAX#36) (HIGH_ORDER_DEFINITION LISPAX#40) (LISTDEF LISPAX#45) (APPENDEF LISPAX#47) (LISTAPPEND LISPAX#48) (ALLPDEF LISPAX#52) (SOMEPDEF LISPAX#53) (MAPCARDEF LISPAX#54) (ALISTDEF1 LISPAX#57) (ALISTDEF LISPAX#58) (ASSOCDEF LISPAX#60) (MEMBERDEF LISPAX#63) (UNIQUENESSDEF LISPAX#65) (PAIRING LISPAX#72) (FRACT0 FRACTIONS#3) (FRACT1 FRACTIONS#4) (FRACT2 FRACTIONS#5) (FRACT4 FRACTIONS#6) (EFDEF FRACTIONS#8) (FRACT3 FRACTIONS#9) (REFLEXF FRACTIONS#10) (SYMMF FRACTIONS#11) (TRANSF FRACTIONS#12) (TRANSF1 FRACTIONS#13) (FR_EQCLASS FRACTIONS#14) (TOTALORDFR FRORDERING#5) (STRICTFR1 FRORDERING#6) (ANTISYMLESS FRORDERING#6) (STRICTLYLESS FRORDERING#6) (STRICTFR2 FRORDERING#7) (STRICTFR3 FRORDERING#8) (GF_LF FRORDERING#9) (EF_LF FRORDERING#10) (LF_EF FRORDERING#11) (LF_EF_EF_LF FRORDERING#12) (GF_EF_EF_GF FRORDERING#13) (GEFDEF FRORDERING#15) (LEFDEF FRORDERING#17) (LANDAU_TH46 FRORDERING#18) (LANDAU_TH47 FRORDERING#19) (GEF_LEF FRORDERING#20) (TRANSORDFR FRORDERING#21) (LANDAU_A_TH51 FRORDERING#22) (LANDAU_B_TH51 FRORDERING#23) (LANDAU_TH52 FRORDERING#24) (NOLASTFR FRORDERING#25) (NOLEASTFR FRORDERING#26) (DENSEFR FRORDERING#27) (QZEROPDEF FRORDERING#30) (QZEROLEAST2 FRORDERING#31) (PLUSFDEF FRACTSUM#2) (PLUSFSORT FRACTSUM#3) (SUMF_UNIQUENESS FRACTSUM#4) (SUMF_SIMPL FRACTSUM#5) (COMMUTFADD FRACTSUM#6) (ASSOCFADD FRACTSUM#7) (SUMF_INCREASING FRACTSUM#8) (LF_SUMFPRESERV FRACTSUM#9) (EF_SUMFPRESERV FRACTSUM#10) (GF_SUMFPRESERV FRACTSUM#11) (GF_SUMFSIMPL FRACTSUM#12) (EF_SUMFSIMPL FRACTSUM#13) (LF_SUMFSIMPL FRACTSUM#14) (GF_GF_SUMFPRESERV FRACTSUM#15) (LEF_LF_SUMFPRESERV FRACTSUM#16) (LF_LEF_SUMFPRESERV FRACTSUM#17) (LEF_LEF_SUMFPRESERV FRACTSUM#18) (PLUS_QZERO FRACTSUM#19) (MINUSDEF FRACTSUM#20) (MINUSDEFINITION FRACTSUM#21) (TIMESFDEF FRACTMULT#2) (PRODF_UNIQUENESS FRACTMULT#4) (COMMUTFPROD FRACTMULT#5) (ASSOCFPROD FRACTMULT#6) (DISTRIBF_LEFT FRACTMULT#7) (GF_PRODFPRESERV FRACTMULT#8) (EF_PRODFPRESERV FRACTMULT#9) (LF_PRODFPRESERV FRACTMULT#10) (GF_PRODFSIMPL FRACTMULT#11) (EF_PRODFSIMPL FRACTMULT#12) (LF_PRODFSIMPL FRACTMULT#13) (GF_GF_PRODFPRESERV FRACTMULT#14) (LEF_LF_PRODFPRESERV FRACTMULT#15) (LF_LEF_PRODFPRESERV FRACTMULT#16) (LEF_LEF_PRODFPRESERV FRACTMULT#17) (INVDEF FRACTMULT#18) (INVSORT FRACTMULT#19) (RTIMES_QONE FRACTMULT#20) (LTIMES_QONE FRACTMULT#21) (FIELD FRACTMULT#22) (TFZF FRACTMULT#23) (DIVISION FRACTMULT#24) (DIVISIONDEFINITION FRACTMULT#25) (RATIO_EXTENSIONALITY RATIONAL#2) (MKRATIO RATIONAL#5) (RATIODEF RATIONAL#6) (REPRESENTDEF RATIONAL#8) (MKREPRESENT RATIONAL#11) (REPRESENT_UNIQUENESS RATIONAL#12) (EQCLASS_UNIQUENESS RATIONAL#13) (TOTALORDRAT ORDRAT#5) (STRICTRAT1 ORDRAT#6) (STRICTRAT2 ORDRAT#7) (STRICTRAT3 ORDRAT#8) (STRICTLYLESSRAT ORDRAT#9) (GRAT_LRAT ORDRAT#10) (ANTISYMLESSRAT ORDRAT#11) (LEQRATDEF1 ORDRAT#16) (GEQRATDEF1 ORDRAT#17) (GEQRAT_LEQRAT ORDRAT#18) (TRANSORDRAT ORDRAT#19) (LANDAU_A_TH87 ORDRAT#20) (LANDAU_B_TH87 ORDRAT#21) (LANDAU_TH88 ORDRAT#22) (NOLASTRAT ORDRAT#23) (NOLEASTRAT ORDRAT#24) (DENSERAT ORDRAT#25) (RZEROPDEF ORDRAT#28) (RONEDEF ORDRAT#31) (RZEROLEAST ORDRAT#32) (RZEROLEAST2 ORDRAT#33) (ADDRAT ADDRAT#2) (REPRESENT_RATSUM ADDRAT#4) (ADDRAT_REDUCTION ADDRAT#5) (COMMADDRAT ADDRAT#6) (ASSOCADDRAT ADDRAT#7) (ADDRAT_INCREASING ADDRAT#8) (ADDRAT_GREATPRESERVING ADDRAT#11) (GREAT_GREAT_ADDRATPRESERVING ADDRAT#13) (LEQ_LEQ_ADDRATPRESERVING ADDRAT#16) (MINUSRAT ADDRAT#17) (PLUS_RZERO ADDRAT#18) (ADD_RZERO ADDRAT#19) (MULTRAT MULTRAT#2) (REPRESENT_RATMULT MULTRAT#4) (RATPROD_REDUCTION MULTRAT#5) (COMMULTRAT MULTRAT#6) (ASSOCMULTRAT MULTRAT#7) (DISTRAT MULTRAT#8) (GREAT_MULTRATPRESERVING MULTRAT#9) (RIGHTRATCANCEL MULTRAT#10) (LESS_MULTRATPRESERVING MULTRAT#11) (LANDAU_TH107 MULTRAT#12) (LANDAU_A_TH108 MULTRAT#13) (LANDAU_B_TH108 MULTRAT#14) (LANDAU_TH109 MULTRAT#15) (DIVDEF MULTRAT#17) (DIVSORT MULTRAT#18) (DIVISIONRAT MULTRAT#19) (LANDAU_TH110 MULTRAT#20) (TIMES_RONE MULTRAT#21) (LANDAU_A_TH111 EMBEDDING#3) (LANDAU_B_TH111 EMBEDDING#4) (LANDAU_C_TH111 EMBEDDING#5) (LANDAU_TH112 EMBEDDING#7) (INTEGERS_PEANO1 EMBEDDING#8) (INTEGERS_PEANO2 EMBEDDING#9) (INTEGERS_PEANO3 EMBEDDING#10) (INTEGERS_PEANO4 EMBEDDING#11) (INTEGER_PEANO5 EMBEDDING#12) (LANDAU_TH114 EMBEDDING#12) (LANDAU_TH115 EMBEDDING#12) (CONS_CAR_CDR LISPAX#28 LISPAX#29) (LEQ_LESS_ADDRATPRESERVING ADDRAT#14 ADDRAT#15) (GREAT_ADDRATPRESERVING ADDRAT#9 ADDRAT#10 ADDRAT#12) (NORMAL NORMAL#1 NORMAL#2 NORMAL#3 NORMAL#4) (TRICOTOMY NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23) (SUCCFACTS NATNUM#6 NATNUM#7 ORDERING#21 ORDERING#29 ORDERING#30) (TIMESFACTS MULTIP#2 MULTIP#4 MULTIP#5 MULTIP#6 MULTIP#7 MULTIP#8 MULTIP#9 MULTIP#10 MULTIP#12 MULTIP#13) (PLUSFACTS NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#22 ORDERING#23 MULTIP#12 MULTIP#13) (SIMPINFO NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#3 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11 ORDRAT#33 ADDRAT#3 ADDRAT#18 ADDRAT#19 MULTRAT#18 MULTIP#2 MULTIP#4 MULTIP#5 MULTIP#6 MULTIP#7 MULTIP#8 MULTIP#9 MULTIP#10 MULTIP#12 MULTIP#13 EMBEDDING#2)) (NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 1 .)(NIL . (DECL (SETVAR SETVAR1) (TYPE: (TY& . |(?ARBITRARY)→TRUTHVAL|))) . ((SETVAR1 . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .)) (SETVAR . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 2 .)(|∀P P1 P2.(P∨P1)∧P2≡P∧P2∨P1∧P2| . (AXIOM (TM& . |∀P P1 P2.(P∨P1)∧P2≡P∧P2∨P1∧P2|)) . ((P2 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P1 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .))) . NIL . (NORMAL#1) . NIL . NORMAL . NIL . 1 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(|NATNUM(0)| . (TRW (TM& . |NATNUM(0)|) NIL) . NIL . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . ORDERING#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 1 .)(NIL . (DECL GREATERP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: >) (BINDINGPOWER: 920)) . ((GREATERP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . >)) . ORDERING#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 2 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . MULTIP#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . MULTIP . NIL . 1 .)(NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . LISPAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 1 .)(NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . LISPAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 2 .)(NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . LISPAX#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 3 .)(NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . LISPAX#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 4 .)(NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . LISPAX#5 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 5 .)(NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . LISPAX#6 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 6 .)(NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . LISPAX#7 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 7 .)(NIL . (DECL (Q Q0 Q1 Q2 Q3 Q01 Q02 Q03) (TYPE: (TY& . GROUND)) (SORT: (TM& . FR))) . ((Q03 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q02 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q01 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q3 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q2 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q1 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q0 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (FR . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . FRACTIONS . NIL . 1 .)(NIL . (DECL EPSILON (TYPE: (TY& . |((@ARB)⊗(@SETVAR))→TRUTHVAL|)) (INFIXNAME: ε) (BINDINGPOWER: 925)) . ((EPSILON . (|((@ARB)⊗(@SETVAR))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#3 . NIL . VARIABLE .)) SETVAR ARB) . NIL . NIL . NIL . SETS . NIL . 3 .)(|∀ARB1 OBJ1.ARB1εOBJ1≡OBJ1(ARB1)| . (DEFINE EPSILON (TM& . |∀ARB1 OBJ1.ARB1εOBJ1≡OBJ1(ARB1)|) NIL) . ((EPSILON . (|((@ARB)⊗(@SETVAR))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#4 . NIL . DEFINED .)) ARB2 ARB1 ARB SETVAR (OBJ1 . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#4 . NIL . VARIABLE .))) . NIL . (SETS#4) . NIL . SETS . NIL . 4 .)(|∀P P1 P2.P2∧(P∨P1)≡P2∧P∨P2∧P1| . (AXIOM (TM& . |∀P P1 P2.P2∧(P∨P1)≡P2∧P∨P2∧P1|)) . (P2 P1 P) . NIL . (NORMAL#2) . NIL . NORMAL . NIL . 2 .)(|∀P P1 P2.P2∧(P∨P1)≡P∧P2∨P1∧P2| . (AXIOM (TM& . |∀P P1 P2.P2∧(P∨P1)≡P∧P2∨P1∧P2|)) . (P2 P1 P) . NIL . (NORMAL#3) . NIL . NORMAL . NIL . 3 .)(|∀P P1 P2.(P∨P1⊃P2)≡(P⊃P2)∧(P1⊃P2)| . (AXIOM (TM& . |∀P P1 P2.(P∨P1⊃P2)≡(P⊃P2)∧(P1⊃P2)|)) . (P2 P1 P) . NIL . (NORMAL#4) . NIL . NORMAL . NIL . 4 .)(|∀P P1.¬(P∨P1)≡¬P∧¬P1| . (AXIOM (TM& . |∀P P1.¬(P∨P1)≡¬P∧¬P1|)) . (P2 P1 P) . NIL . (NORMAL#5) . NIL . NORMAL . NIL . 5 .)(|∀P P1.¬(P∧P1)≡¬P∨¬P1| . (AXIOM (TM& . |∀P P1.¬(P∧P1)≡¬P∨¬P1|)) . (P2 P1 P) . NIL . (NORMAL#6) . NIL . NORMAL . NIL . 6 .)(|∀P P1.P≡(P1⊃P)∧(¬P1⊃P)| . (AXIOM (TM& . |∀P P1.P≡(P1⊃P)∧(¬P1⊃P)|)) . (P2 P1 P) . NIL . (NORMAL#7) . NIL . NORMAL . NIL . 7 .)(|∀P P1 P2.(P1⊃P2)∧(IF P THEN P1 ELSE P2)⊃P2| . (AXIOM (TM& . |∀P P1 P2.(P1⊃P2)∧(IF P THEN P1 ELSE P2)⊃P2|)) . (P2 P1 P) . NIL . (NORMAL#8) . NIL . NORMAL . NIL . 8 .)(|∀P1 P2 P3 P4.(P2≡P4)∧(P1∨P2∨P3)⊃P1∨P4∨P3| . (AXIOM (TM& . |∀P1 P2 P3 P4.(P2≡P4)∧(P1∨P2∨P3)⊃P1∨P4∨P3|)) . (P2 P1 P (P4 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . NORMAL#9 . NIL . VARIABLE .)) (P3 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . NORMAL#9 . NIL . VARIABLE .))) . NIL . (NORMAL#9) . NIL . NORMAL . NIL . 9 .)(|∀P P1 P2.P∧P1⊃¬P2≡¬(P∧P1∧P2)| . (AXIOM (TM& . |∀P P1 P2.P∧P1⊃¬P2≡¬(P∧P1∧P2)|)) . (P2 P1 P) . NIL . (NORMAL#10) . NIL . NORMAL . NIL . 10 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (M N K J I ADD1) . NIL . (NATNUM#5) . NIL . NATNUM . NIL . 5 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (M N K J I ADD1) . NIL . (NATNUM#6) . NIL . NATNUM . NIL . 6 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (M N K J I ADD1) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& . LISTP))) . ((W . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (V . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (U . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) LISTP) . NIL . NIL . NIL . LISPAX . NIL . 8 .)(NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((Z . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (Y . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . LISPAX . NIL . 9 .)(NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM))) . ((ZA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (YA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (XA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) ATOM) . NIL . NIL . NIL . LISPAX . NIL . 10 .)(NIL . (DECL (PHI) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 11 .)(NIL . (DECL CONS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . LISPAX#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 12 .)(|∀Q.LISTP Q| . (AXIOM (TM& . |∀Q.LISTP Q|)) . (LISTP FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#2) . NIL . FRACTIONS . NIL . 2 .)(NIL . (DECL ALL (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#1 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . ALL . NIL . 1 .)(NIL . (DECL SOME (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#2 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . ALL . NIL . 2 .)(|∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))| . (DEFAX ALL (TM& . |∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))|)) . ((ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#3 . NIL . DEFINED .)) M N K J I SET C B A ADD1) . NIL . (ALL#3) . NIL . ALL . NIL . 3 .)(|∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))| . (DEFAX SOME (TM& . |∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))|)) . ((SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#4 . NIL . DEFINED .)) M N K J I SET C B A ADD1) . NIL . (ALL#4) . NIL . ALL . NIL . 4 .)(NIL . (DECL GF (TYPE: (TY& . |((@Q)⊗(@Q))→TRUTHVAL|))) . ((GF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#1 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRORDERING . NIL . 1 .)(NIL . (DECL PF (TYPE: (TY& . |((@Q)⊗(@Q))→(@Q)|)) (BINDINGPOWER: 940)) . ((PF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940)) . FRACTSUM#1 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRACTSUM . NIL . 1 .)(NIL . (DECL TF (TYPE: (TY& . |((@Q)⊗(@Q))→(@Q)|)) (BINDINGPOWER: 935)) . ((TF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 935)) . FRACTMULT#1 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRACTMULT . NIL . 1 .)(NIL . (DECL (R R0 R1 R2) (TYPE: (TY& . |(@Q)→TRUTHVAL|)) (SORT: (TM& . RATIO))) . ((R2 . (|(@Q)→TRUTHVAL| . (SYMBOL& RATIO NIL) . NIL . NIL . RATIONAL#1 . NIL . VARIABLE .)) (R1 . (|(@Q)→TRUTHVAL| . (SYMBOL& RATIO NIL) . NIL . NIL . RATIONAL#1 . NIL . VARIABLE .)) (R0 . (|(@Q)→TRUTHVAL| . (SYMBOL& RATIO NIL) . NIL . NIL . RATIONAL#1 . NIL . VARIABLE .)) (R . (|(@Q)→TRUTHVAL| . (SYMBOL& RATIO NIL) . NIL . NIL . RATIONAL#1 . NIL . VARIABLE .)) (RATIO . (|(GROUND→TRUTHVAL)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . RATIONAL#1 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . RATIONAL . NIL . 1 .)(|∀SETVAR SETVAR1.(∀ARB.ARBεSETVAR≡ARBεSETVAR1)⊃SETVAR=SETVAR1| . (AXIOM (TM& . |∀SETVAR SETVAR1.(∀ARB.ARBεSETVAR≡ARBεSETVAR1)⊃SETVAR=SETVAR1|)) . (ARB2 ARB1 ARB SETVAR1 SETVAR EPSILON OBJ1) . NIL . (SETS#5) . NIL . SETS . NIL . 5 .)(NIL . (DECL FUNCTION (TYPE: (TY& . |((?ARBITRARY)*)→(?ARBITRARY)|)) (SYNTYPE: VARIABLE)) . ((FUNCTION . (|((?ARBITRARY)*)→(?ARBITRARY)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 6 .)(NIL . (DECL ZETA (TYPE: (TY& . |((?ARBITRARY)*)→TRUTHVAL|)) (SYNTYPE: VARIABLE)) . ((ZETA . (|((?ARBITRARY)*)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 7 .)(NIL . (DECL PARVAR (TYPE: (TY& . ?ARBITRARY)) (SYNTYPE: VARIABLE)) . ((PARVAR . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#8 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 8 .)(|∀M N.¬M=N⊃¬M'=N'| . (DERIVE (TM& . |∀M N.¬M=N⊃¬M'=N'|) ((LR& NATNUM#7)) NIL) . (M N K J I ADD1) . NIL . (NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 9 .)(|∀N.¬N=N'| . (UE (UELST& (A . |λN.¬N=N'|)) (LN& . NATNUM#8) (USE (LR& NATNUM#7))) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8 NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 10 .)(|∀N.¬N=0⊃(∃K.N=K')| . (UE (UELST& (A . |λN.¬N=0⊃(∃K.N=K')|)) (LN& . NATNUM#8) NIL) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8 NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 11 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 12 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#13 . NIL . DEFINED .)) M N K J I ADD1) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|∀XA.SEXP XA| . (AXIOM (TM& . |∀XA.SEXP XA|)) . (ATOM SEXP ZA YA XA) . NIL . (LISPAX#13) . NIL . LISPAX . NIL . 13 .)(|∀U.SEXP U| . (AXIOM (TM& . |∀U.SEXP U|)) . (LISTP SEXP W V U) . NIL . (LISPAX#14) . NIL . LISPAX . NIL . 14 .)(|∀X U.LISTP X.U| . (AXIOM (TM& . |∀X U.LISTP X.U|)) . (LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#15) . NIL . LISPAX . NIL . 15 .)(|∀U.¬NULL U⊃LISTP CDR U| . (AXIOM (TM& . |∀U.¬NULL U⊃LISTP CDR U|)) . (CDR NULL LISTP W V U) . NIL . (LISPAX#16) . NIL . LISPAX . NIL . 16 .)(|∀U.¬NULL U⊃SEXP CAR U| . (AXIOM (TM& . |∀U.¬NULL U⊃SEXP CAR U|)) . (CAR NULL LISTP SEXP W V U) . NIL . (LISPAX#17) . NIL . LISPAX . NIL . 17 .)(|∀X.¬ATOM X⊃SEXP CAR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CAR X|)) . (CAR ATOM SEXP Z Y X) . NIL . (LISPAX#18) . NIL . LISPAX . NIL . 18 .)(|∀X.¬ATOM X⊃SEXP CDR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CDR X|)) . (CDR ATOM SEXP Z Y X) . NIL . (LISPAX#19) . NIL . LISPAX . NIL . 19 .)(|∀X Y.SEXP X.Y| . (AXIOM (TM& . |∀X Y.SEXP X.Y|)) . (SEXP Z Y X CONS) . NIL . (LISPAX#20) . NIL . LISPAX . NIL . 20 .)(|∀X Y.¬ATOM X.Y| . (AXIOM (TM& . |∀X Y.¬ATOM X.Y|)) . (ATOM SEXP Z Y X CONS) . NIL . (LISPAX#21) . NIL . LISPAX . NIL . 21 .)(|∀X U.¬NULL X.U| . (AXIOM (TM& . |∀X U.¬NULL X.U|)) . (NULL LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#22) . NIL . LISPAX . NIL . 22 .)(|∀U.NULL U⊃U=NIL| . (AXIOM (TM& . |∀U.NULL U⊃U=NIL|)) . (NULL LISTP W V U) . NIL . (LISPAX#23) . NIL . LISPAX . NIL . 23 .)(|∀X Y.CAR (X.Y)=X| . (AXIOM (TM& . |∀X Y.CAR (X.Y)=X|)) . (CAR SEXP Z Y X CONS) . NIL . (LISPAX#24) . NIL . LISPAX . NIL . 24 .)(|∀X Y.CDR (X.Y)=Y| . (AXIOM (TM& . |∀X Y.CDR (X.Y)=Y|)) . (CDR SEXP Z Y X CONS) . NIL . (LISPAX#25) . NIL . LISPAX . NIL . 25 .)(|CAR NIL=NIL| . (AXIOM (TM& . |CAR NIL=NIL|)) . (CAR) . NIL . (LISPAX#26) . NIL . LISPAX . NIL . 26 .)(|CDR NIL=NIL| . (AXIOM (TM& . |CDR NIL=NIL|)) . (CDR) . NIL . (LISPAX#27) . NIL . LISPAX . NIL . 27 .)(|∀U.¬NULL U⊃CAR U.CDR U=U| . (AXIOM (TM& . |∀U.¬NULL U⊃CAR U.CDR U=U|)) . (CAR CDR NULL LISTP W V U CONS) . NIL . (LISPAX#28) . NIL . LISPAX . NIL . 28 .)(|∀X.¬ATOM X⊃CAR X.CDR X=X| . (AXIOM (TM& . |∀X.¬ATOM X⊃CAR X.CDR X=X|)) . (CAR CDR ATOM SEXP Z Y X CONS) . NIL . (LISPAX#29) . NIL . LISPAX . NIL . 29 .)(|∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))| . (AXIOM (TM& . |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)) . (LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30) . NIL . LISPAX . NIL . 30 .)(NIL . (DECL PARS (TYPE: (TY& . GROUND*))) . ((PARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 31 .)(NIL . (DECL (DF DF1 DF2) (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((DF2 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF1 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 32 .)(NIL . (DECL NILCASE (TYPE: (TY& . |(GROUND*)→(GROUND*)|))) . ((NILCASE . (|(GROUND*)→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#33 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 33 .)(|∀R R1.(∀Q.R(Q)≡R1(Q))⊃R=R1| . (AXIOM (TM& . |∀R R1.(∀Q.R(Q)≡R1(Q))⊃R=R1|)) . (Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR RATIO R2 R1 R0 R) . NIL . (RATIONAL#2) . NIL . RATIONAL . NIL . 2 .)(NIL . (DECL (EQCLASS) (TYPE: (TY& . |(@Q)→(@R)|))) . ((EQCLASS . (|(@Q)→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . RATIONAL#3 . NIL . VARIABLE .)) R Q) . NIL . NIL . NIL . RATIONAL . NIL . 3 .)(NIL . (DECL GREATRAT (TYPE: (TY& . |((@R)⊗(@R))→TRUTHVAL|)) (INFIXNAME: >>) (SYNTYPE: CONSTANT) (BINDINGPOWER: 945)) . ((GREATRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . >>)) . ORDRAT#1 . NIL . CONSTANT .)) R) . NIL . NIL . NIL . ORDRAT . NIL . 1 .)(NIL . (DECL ADDRAT (TYPE: (TY& . |((@R)*)→(@R)|)) (INFIXNAME: ++) (BINDINGPOWER: 948)) . ((ADDRAT . (|((@R)*)→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 948) (INFIX& . ++)) . ADDRAT#1 . NIL . VARIABLE .)) R) . NIL . NIL . NIL . ADDRAT . NIL . 1 .)(NIL . (DECL MULTRAT (TYPE: (TY& . |((@R)*)→(@R)|)) (INFIXNAME: **) (BINDINGPOWER: 949)) . ((MULTRAT . (|((@R)*)→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 949) (INFIX& . **)) . MULTRAT#1 . NIL . VARIABLE .)) R) . NIL . NIL . NIL . MULTRAT . NIL . 1 .)(|(∀ARB1.(∃ARB2.ZETA(ARB1,ARB2,PARVAR)))⊃(∃FUNCTION.(∀ARB1.ZETA(ARB1,FUNCTION(ARB1,PARVAR),PARVAR)))| . (AXIOM (TM& . |(∀ARB1.(∃ARB2.ZETA(ARB1,ARB2,PARVAR)))⊃(∃FUNCTION.(∀ARB1.ZETA(ARB1,FUNCTION(ARB1,PARVAR),PARVAR)))|)) . (ARB2 ARB1 ARB FUNCTION ZETA PARVAR) . NIL . (SETS#9) . NIL . SETS . NIL . 9 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N M.(∃K.K=N+M∧(∀I J.I=M+N∧J=M+N⊃I=J))| . (AXIOM (TM& . |∀N M.(∃K.K=N+M∧(∀I J.I=M+N∧J=M+N⊃I=J))|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(|∀N M.¬N=N+M'| . (AXIOM (TM& . |∀N M.¬N=N+M'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#18) . NIL . NATNUM . NIL . 18 .)(|∀N K M.¬K=M⊃¬N+K=N+M| . (AXIOM (TM& . |∀N K M.¬K=M⊃¬N+K=N+M|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀N M.M=N∨(∃K.M=N+K')∨(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.M=N∨(∃K.M=N+K')∨(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N M.M=N⊃¬(∃K.M=N+K')∧¬(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.M=N⊃¬(∃K.M=N+K')∧¬(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀N M.(∃K.M=N+K')⊃¬M=N∧¬(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.(∃K.M=N+K')⊃¬M=N∧¬(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N M.(∃K.N=M+K')⊃¬M=N∧¬(∃K.M=N+K')| . (AXIOM (TM& . |∀N M.(∃K.N=M+K')⊃¬M=N∧¬(∃K.M=N+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀N M.N>M≡(∃K.N=M+K')| . (DEFAX GREATERP (TM& . |∀N M.N>M≡(∃K.N=M+K')|)) . ((GREATERP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . >)) . ORDERING#3 . NIL . DEFINED .)) M N K J I ADD1 PLUS) . NIL . (ORDERING#3) . NIL . ORDERING . NIL . 3 .)(|∀N M.N<M≡(∃K.M=N+K')| . (DEFAX LESSP (TM& . |∀N M.N<M≡(∃K.M=N+K')|)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . ORDERING#4 . NIL . DEFINED .)) M N K J I ADD1 PLUS) . NIL . (ORDERING#4) . NIL . ORDERING . NIL . 4 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . MULTIP#2 . NIL . DEFINED .)) M N K J I ADD1 PLUS) . NIL . (MULTIP#2) . NIL . MULTIP . NIL . 2 .)(|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))| . (AXIOM (TM& . |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)) . (LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .)) (DEF . (|(GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .))) . NIL . (LISPAX#34) . NIL . LISPAX . NIL . 34 .)(|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))| . (AXIOM (TM& . |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)) . (ATOM SEXP Z Y X PHI CONS) . NIL . (LISPAX#35) . NIL . LISPAX . NIL . 35 .)(|∀N M.M<N∨M=N∨M>N| . (AXIOM (TM& . |∀N M.M<N∨M=N∨M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#5) . NIL . ORDERING . NIL . 5 .)(|∀N M.M=N⊃¬M<N∧¬M>N| . (AXIOM (TM& . |∀N M.M=N⊃¬M<N∧¬M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#6) . NIL . ORDERING . NIL . 6 .)(|∀N M.M>N⊃¬M=N∧¬M<N| . (AXIOM (TM& . |∀N M.M>N⊃¬M=N∧¬M<N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#7) . NIL . ORDERING . NIL . 7 .)(|∀N M.M<N⊃¬M=N∧¬M>N| . (AXIOM (TM& . |∀N M.M<N⊃¬M=N∧¬M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#8) . NIL . ORDERING . NIL . 8 .)(|∀N M.M>N≡N<M| . (AXIOM (TM& . |∀N M.M>N≡N<M|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#9) . NIL . ORDERING . NIL . 9 .)(NIL . (DECL GRTEQP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: ≥) (BINDINGPOWER: 920)) . ((GRTEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≥)) . ORDERING#10 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 10 .)(NIL . (DECL LSSEQP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: ≤) (BINDINGPOWER: 920)) . ((LSSEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . ORDERING#11 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 11 .)(|∀N M.M≥N≡M>N∨M=N| . (DEFAX GRTEQP (TM& . |∀N M.M≥N≡M>N∨M=N|)) . ((GRTEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≥)) . ORDERING#12 . NIL . DEFINED .)) M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#12) . NIL . ORDERING . NIL . 12 .)(|∀N M.M≤N≡M<N∨M=N| . (DEFAX LSSEQP (TM& . |∀N M.M≤N≡M<N∨M=N|)) . ((LSSEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . ORDERING#13 . NIL . DEFINED .)) M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#13) . NIL . ORDERING . NIL . 13 .)(|∀N M.NATNUM(N*M)| . (AXIOM (TM& . |∀N M.NATNUM(N*M)|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#3) . NIL . MULTIP . NIL . 3 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#4) . NIL . MULTIP . NIL . 4 .)(|∀K N.N*K'=N*K+N| . (AXIOM (TM& . |∀K N.N*K'=N*K+N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#5) . NIL . MULTIP . NIL . 5 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#6) . NIL . MULTIP . NIL . 6 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#7) . NIL . MULTIP . NIL . 7 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#8) . NIL . MULTIP . NIL . 8 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#9) . NIL . MULTIP . NIL . 9 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#10) . NIL . MULTIP . NIL . 10 .)(|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))| . (AXIOM (TM& . |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))|)) . (ATOM LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE FUN DEF (DEFSEXP . (|(GROUND⊗GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .)) (ATOMCASE . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .))) . NIL . (LISPAX#36) . NIL . LISPAX . NIL . 36 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 37 .)(|∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)| . (AXIOM (TM& . |∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)|)) . (M N K J I SET C B A ADD1 PLUS LESSP ALL) . NIL . (ALL#5) . NIL . ALL . NIL . 5 .)(|∀A N.(∃M.M<N∧A(M))≡SOME(N,A)| . (AXIOM (TM& . |∀A N.(∃M.M<N∧A(M))≡SOME(N,A)|)) . (M N K J I SET C B A ADD1 PLUS LESSP SOME) . NIL . (ALL#6) . NIL . ALL . NIL . 6 .)(|∀N M.M≥N≡N≤M| . (AXIOM (TM& . |∀N M.M≥N≡N≤M|)) . (M N K J I ADD1 PLUS LESSP GREATERP GRTEQP LSSEQP) . NIL . (ORDERING#14) . NIL . ORDERING . NIL . 14 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#15) . NIL . ORDERING . NIL . 15 .)(|∀N M K.K>M∧M>N⊃K>N| . (AXIOM (TM& . |∀N M K.K>M∧M>N⊃K>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#16) . NIL . ORDERING . NIL . 16 .)(|∀N M K.N≤M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N≤M∧M<K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#17) . NIL . ORDERING . NIL . 17 .)(|∀N M K.N<M∧M≤K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M≤K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#18) . NIL . ORDERING . NIL . 18 .)(|∀N M K.N≤M∧M≤K⊃N≤K| . (AXIOM (TM& . |∀N M K.N≤M∧M≤K⊃N≤K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#19) . NIL . ORDERING . NIL . 19 .)(|∀N M.N+M'>N| . (AXIOM (TM& . |∀N M.N+M'>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#20) . NIL . ORDERING . NIL . 20 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#21) . NIL . ORDERING . NIL . 21 .)(|∀N M K.M+K>N+K≡M>N| . (AXIOM (TM& . |∀N M K.M+K>N+K≡M>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#22) . NIL . ORDERING . NIL . 22 .)(|∀N M K.M+K<N+K≡M<N| . (AXIOM (TM& . |∀N M K.M+K<N+K≡M<N|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#23) . NIL . ORDERING . NIL . 23 .)(|∀N M I J.N>M∧I>J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N>M∧I>J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#24) . NIL . ORDERING . NIL . 24 .)(|∀N M I J.N≥M∧I>J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N≥M∧I>J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#25) . NIL . ORDERING . NIL . 25 .)(|∀N M I J.N>M∧I≥J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N>M∧I≥J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#26) . NIL . ORDERING . NIL . 26 .)(|∀N M I J.N≥M∧I≥J⊃N+I≥M+J| . (AXIOM (TM& . |∀N M I J.N≥M∧I≥J⊃N+I≥M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#27) . NIL . ORDERING . NIL . 27 .)(|∀N.N≥0| . (AXIOM (TM& . |∀N.N≥0|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#28) . NIL . ORDERING . NIL . 28 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#29) . NIL . ORDERING . NIL . 29 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#30) . NIL . ORDERING . NIL . 30 .)(|∀N.N'≥1| . (AXIOM (TM& . |∀N.N'≥1|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#31) . NIL . ORDERING . NIL . 31 .)(|∀N M.N>M⊃N≥M'| . (AXIOM (TM& . |∀N M.N>M⊃N≥M'|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#32) . NIL . ORDERING . NIL . 32 .)(|∀M N.M<N'⊃M≤N| . (AXIOM (TM& . |∀M N.M<N'⊃M≤N|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#33) . NIL . ORDERING . NIL . 33 .)(|∀A.(∃M.A(M))⊃(∃N.A(N)∧(∀M.A(M)⊃N<M))| . (AXIOM (TM& . |∀A.(∃M.A(M))⊃(∃N.A(N)∧(∀M.A(M)⊃N<M))|)) . (M N K J I SET C B A ADD1 PLUS LESSP) . NIL . (ORDERING#34) . NIL . ORDERING . NIL . 34 .)(NIL . (DECL BIGFUN (TYPE: (TY& . |(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)|))) . ((BIGFUN . (|(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#38 . NIL . VARIABLE .)) (ARB . LISPAX#37)) . NIL . NIL . NIL . LISPAX . NIL . 38 .)(NIL . (DECL (DEFINED_FUN ATOM_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((ATOM_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) (DEFINED_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) (ARB . LISPAX#37)) . NIL . NIL . NIL . LISPAX . NIL . 39 .)(¬N=0∧¬M=0⊃¬N*M=0 . (DERIVE (TM& . ¬N=0∧¬M=0⊃¬N*M=0) ((LR& MULTIP#10)) NIL) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#10 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4) . NIL . MULTIP . NIL . 11 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#12) . NIL . MULTIP . NIL . 12 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#13) . NIL . MULTIP . NIL . 13 .)(|∀N M K.N>M∧¬K=0⊃N*K>M*K| . (AXIOM (TM& . |∀N M K.N>M∧¬K=0⊃N*K>M*K|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#14) . NIL . MULTIP . NIL . 14 .)(|∀N M K.N<M∧¬K=0⊃N*K<M*K| . (AXIOM (TM& . |∀N M K.N<M∧¬K=0⊃N*K<M*K|)) . (M N K J I ADD1 PLUS LESSP TIMES) . NIL . (MULTIP#15) . NIL . MULTIP . NIL . 15 .)(|∀N M K.¬K=0∧M*K>N*K⊃M>N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K>N*K⊃M>N|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#16) . NIL . MULTIP . NIL . 16 .)(|∀N M K.¬K=0∧M*K=N*K⊃M=N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K=N*K⊃M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#17) . NIL . MULTIP . NIL . 17 .)(|∀N M K.¬K=0∧M*K<N*K⊃M<N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K<N*K⊃M<N|)) . (M N K J I ADD1 PLUS LESSP TIMES) . NIL . (MULTIP#18) . NIL . MULTIP . NIL . 18 .)(|∀N M I J.N>M∧I>J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.N>M∧I>J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#19) . NIL . MULTIP . NIL . 19 .)(|∀N M I J.¬M=0∧N≥M∧I>J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.¬M=0∧N≥M∧I>J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#20) . NIL . MULTIP . NIL . 20 .)(|∀N M I J.¬J=0∧N>M∧I≥J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.¬J=0∧N>M∧I≥J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#21) . NIL . MULTIP . NIL . 21 .)(|∀N M I J.N≥M∧I≥J⊃N*I≥M*J| . (AXIOM (TM& . |∀N M I J.N≥M∧I≥J⊃N*I≥M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#22) . NIL . MULTIP . NIL . 22 .)(|∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))| . (AXIOM (TM& . |∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))|)) . (ATOM SEXP Z Y X CONS (ARB . LISPAX#37) BIGFUN ATOM_FUN DEFINED_FUN) . NIL . (LISPAX#40) . NIL . LISPAX . NIL . 40 .)(NIL . (DECL LIST (TYPE: (TY& . |(GROUND*)→GROUND|)) (SYNTYPE: CONSTANT)) . ((LIST . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#41 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 41 .)(NIL . (DECL LST (TYPE: (TY& . GROUND*))) . ((LST . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#42 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 42 .)(|LIST(())=NIL| . (AXIOM (TM& . |LIST(())=NIL|)) . (LIST) . NIL . (LISPAX#43) . NIL . LISPAX . NIL . 43 .)(|∀LST.LISTP LIST(LST)| . (AXIOM (TM& . |∀LST.LISTP LIST(LST)|)) . (LISTP LIST LST) . NIL . (LISPAX#44) . NIL . LISPAX . NIL . 44 .)(|∀X LST.LIST(X,LST)=X.LIST(LST)| . (AXIOM (TM& . |∀X LST.LIST(X,LST)=X.LIST(LST)|)) . (SEXP Z Y X CONS LIST LST) . NIL . (LISPAX#45) . NIL . LISPAX . NIL . 45 .)(NIL . (DECL APPEND (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: **) (BINDINGPOWER: 840)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . **)) . LISPAX#46 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 46 .)(|∀X U V.NIL ** V=V∧X.U ** V=X.(U ** V)| . (DEFAX APPEND (TM& . |∀X U V.NIL ** V=V∧X.U ** V=X.(U ** V)|)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . **)) . LISPAX#47 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#47) . NIL . LISPAX . NIL . 47 .)(|∀U V.LISTP U ** V| . (AXIOM (TM& . |∀U V.LISTP U ** V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#48) . NIL . LISPAX . NIL . 48 .)(|∀U.U ** NIL=U| . (AXIOM (TM& . |∀U.U ** NIL=U|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#49) . NIL . LISPAX . NIL . 49 .)(|∀X V.X.NIL ** V=X.V| . (AXIOM (TM& . |∀X V.X.NIL ** V=X.V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#50) . NIL . LISPAX . NIL . 50 .)(NIL . (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@PHI)⊗GROUND)→TRUTHVAL|))) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) PHI) . NIL . NIL . NIL . LISPAX . NIL . 51 .)(|∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)| . (DEFAX ALLP (TM& . |∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)) . ((ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS (SOMEP . LISPAX#51)) . NIL . (LISPAX#52) . NIL . LISPAX . NIL . 52 .)(|∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))| . (DEFAX SOMEP (TM& . |∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#53 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#53) . NIL . LISPAX . NIL . 53 .)(|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)| . (DEFAX MAPCAR (TM& . |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)) . ((MAPCAR . (|((GROUND→GROUND)⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS (FN . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . VARIABLE .))) . NIL . (LISPAX#54) . NIL . LISPAX . NIL . 54 .)(NIL . (DECL (ALIST) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((ALIST . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#55 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . LISPAX . NIL . 55 .)(|∀ALIST.LISTP ALIST| . (AXIOM (TM& . |∀ALIST.LISTP ALIST|)) . (LISTP ALISTP ALIST) . NIL . (LISPAX#56) . NIL . LISPAX . NIL . 56 .)(|∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)| . (AXIOM (TM& . |∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)|)) . (CAR CDR ATOM NULL LISTP ALISTP W V U) . NIL . (LISPAX#57) . NIL . LISPAX . NIL . 57 .)(|∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST| . (AXIOM (TM& . |∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#58) . NIL . LISPAX . NIL . 58 .)(NIL . (DECL ASSOC (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#59 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 59 .)(|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))| . (DEFAX ASSOC (TM& . |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#60 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#60) . NIL . LISPAX . NIL . 60 .)(|∀X ALIST.SEXP ASSOC(X,ALIST)| . (AXIOM (TM& . |∀X ALIST.SEXP ASSOC(X,ALIST)|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC) . NIL . (LISPAX#61) . NIL . LISPAX . NIL . 61 .)(NIL . (DECL MEMBER (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#62 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 62 .)(|∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))| . (DEFAX MEMBER (TM& . |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#63 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#63) . NIL . LISPAX . NIL . 63 .)(NIL . (DECL UNIQUENESS (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#64 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 64 .)(|∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))| . (DEFAX UNIQUENESS (TM& . |∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))|)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#65 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS MEMBER) . NIL . (LISPAX#65) . NIL . LISPAX . NIL . 65 .)(|∀U.SEXP CAR U| . (UE (UELST& (PHI . |λU.SEXP CAR U|)) (LN& . LISPAX#30) NIL) . (CAR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61) . NIL . LISPAX . NIL . 66 .)(|∀U.LISTP CDR U| . (UE (UELST& (PHI . |λU.LISTP CDR U|)) (LN& . LISPAX#30) NIL) . (CDR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66) . NIL . LISPAX . NIL . 67 .)(|CADR=(λXV.CAR (CDR XV))| . (DEFINE CADR (TM& . |CADR=(λXV.CAR (CDR XV))|) NIL) . ((CADR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#68 . NIL . DEFINED .)) CAR CDR SEXP (XV . (GROUND . (SYMBOL& SEXP NIL) . NIL . ((BINDP& . 1000)) . LISPAX#68 . NIL . VARIABLE .))) . NIL . (LISPAX#68 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67) . NIL . LISPAX . NIL . 68 .)(|CDDR=(λXV.CDR (CDR XV))| . (DEFINE CDDR (TM& . |CDDR=(λXV.CDR (CDR XV))|) NIL) . ((CDDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#69 . NIL . DEFINED .)) CAR CDR SEXP XV CADR) . NIL . (LISPAX#69 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67) . NIL . LISPAX . NIL . 69 .)(|∀U.SEXP CAR U| . (AXIOM (TM& . |∀U.SEXP CAR U|)) . (CAR LISTP SEXP W V U) . NIL . (LISPAX#70) . NIL . LISPAX . NIL . 70 .)(|∀U.LISTP CDR U| . (AXIOM (TM& . |∀U.LISTP CDR U|)) . (CDR LISTP W V U) . NIL . (LISPAX#71) . NIL . LISPAX . NIL . 71 .)(|∀U.¬NULL CADR(U)∧NULL CDDR(U)⊃LIST(CAR U,CADR(U))=U| . (AXIOM (TM& . |∀U.¬NULL CADR(U)∧NULL CDDR(U)⊃LIST(CAR U,CADR(U))=U|)) . (CAR CDR NULL LISTP SEXP W V U LIST XV CADR CDDR) . NIL . (LISPAX#72) . NIL . LISPAX . NIL . 72 .)(|∀N.¬NULL N| . (AXIOM (TM& . |∀N.¬NULL N|)) . (M N K J I NULL) . NIL . (LISPAX#73) . NIL . LISPAX . NIL . 73 .)(|∀N.SEXP N| . (AXIOM (TM& . |∀N.SEXP N|)) . (M N K J I SEXP) . NIL . (LISPAX#74) . NIL . LISPAX . NIL . 74 .)(|∀X Y.CAR LIST(X,Y)=X| . (AXIOM (TM& . |∀X Y.CAR LIST(X,Y)=X|)) . (CAR SEXP Z Y X LIST) . NIL . (LISPAX#75) . NIL . LISPAX . NIL . 75 .)(|∀X Y.CADR(LIST(X,Y))=Y| . (AXIOM (TM& . |∀X Y.CADR(LIST(X,Y))=Y|)) . (CAR CDR SEXP Z Y X LIST XV CADR) . NIL . (LISPAX#76) . NIL . LISPAX . NIL . 76 .)(|∀Q.NULL CDDR(Q)| . (AXIOM (TM& . |∀Q.NULL CDDR(Q)|)) . (CAR CDR NULL SEXP XV CADR CDDR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#3) . NIL . FRACTIONS . NIL . 3 .)(|∀M N.¬N=0⊃FR(LIST(M,N))| . (AXIOM (TM& . |∀M N.¬N=0⊃FR(LIST(M,N))|)) . (M N K J I LIST FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#4) . NIL . FRACTIONS . NIL . 4 .)(|∀Q.NATNUM(CAR Q)∧NATNUM(CADR(Q))∧¬CADR(Q)=0| . (AXIOM (TM& . |∀Q.NATNUM(CAR Q)∧NATNUM(CADR(Q))∧¬CADR(Q)=0|)) . (CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#5) . NIL . FRACTIONS . NIL . 5 .)(|∀Q.LIST(CAR Q,CADR(Q))=Q| . (AXIOM (TM& . |∀Q.LIST(CAR Q,CADR(Q))=Q|)) . (CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#6) . NIL . FRACTIONS . NIL . 6 .)(NIL . (DECL EF (TYPE: (TY& . |((@Q)⊗(@Q))→TRUTHVAL|))) . ((EF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTIONS#7 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRACTIONS . NIL . 7 .)(|EF=(λQ Q0.(IF CAR Q*CADR(Q0)=CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))| . (DEFINE EF (TM& . |EF=(λQ Q0.(IF CAR Q*CADR(Q0)=CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))|) NIL) . ((EF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTIONS#8 . NIL . DEFINED .)) M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#8 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6) . NIL . FRACTIONS . NIL . 8 .)(|∀Q.FR(LIST(CAR Q,CADR(Q)))| . (AXIOM (TM& . |∀Q.FR(LIST(CAR Q,CADR(Q)))|)) . (CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#9) . NIL . FRACTIONS . NIL . 9 .)(|∀Q.EF(Q,Q)| . (AXIOM (TM& . |∀Q.EF(Q,Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#10) . NIL . FRACTIONS . NIL . 10 .)(|∀Q Q0.EF(Q,Q0)⊃EF(Q0,Q)| . (AXIOM (TM& . |∀Q Q0.EF(Q,Q0)⊃EF(Q0,Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#11) . NIL . FRACTIONS . NIL . 11 .)(|∀Q Q1 Q2.EF(Q,Q1)∧EF(Q1,Q2)⊃EF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.EF(Q,Q1)∧EF(Q1,Q2)⊃EF(Q,Q2)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#12) . NIL . FRACTIONS . NIL . 12 .)(|∀Q Q1 Q2 Q3.EF(Q,Q1)∧EF(Q1,Q2)∧EF(Q2,Q3)⊃EF(Q,Q3)| . (AXIOM (TM& . |∀Q Q1 Q2 Q3.EF(Q,Q1)∧EF(Q1,Q2)∧EF(Q2,Q3)⊃EF(Q,Q3)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#13) . NIL . FRACTIONS . NIL . 13 .)(|∀Q N.¬N=0⊃EF(LIST(CAR Q*N,CADR(Q)*N),Q)| . (AXIOM (TM& . |∀Q N.¬N=0⊃EF(LIST(CAR Q*N,CADR(Q)*N),Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#14) . NIL . FRACTIONS . NIL . 14 .)(|GF=(λQ Q0.(IF CAR Q*CADR(Q0)>CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))| . (DEFINE GF (TM& . |GF=(λQ Q0.(IF CAR Q*CADR(Q0)>CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))|) NIL) . ((GF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#2 . NIL . DEFINED .)) M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRORDERING#2 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9) . NIL . FRORDERING . NIL . 2 .)(NIL . (DECL LF (TYPE: (TY& . |((@Q)⊗(@Q))→TRUTHVAL|))) . ((LF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#3 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRORDERING . NIL . 3 .)(|LF=(λQ Q0.(IF CAR Q*CADR(Q0)<CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))| . (DEFINE LF (TM& . |LF=(λQ Q0.(IF CAR Q*CADR(Q0)<CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))|) NIL) . ((LF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#4 . NIL . DEFINED .)) M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRORDERING#4 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9) . NIL . FRORDERING . NIL . 4 .)(|∀Q Q0.LF(Q,Q0)∨EF(Q,Q0)∨GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.LF(Q,Q0)∨EF(Q,Q0)∨GF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#5) . NIL . FRORDERING . NIL . 5 .)(|∀Q Q0.EF(Q,Q0)⊃¬LF(Q,Q0)∧¬GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.EF(Q,Q0)⊃¬LF(Q,Q0)∧¬GF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#6) . NIL . FRORDERING . NIL . 6 .)(|∀Q Q0.GF(Q,Q0)⊃¬EF(Q,Q0)∧¬LF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.GF(Q,Q0)⊃¬EF(Q,Q0)∧¬LF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#7) . NIL . FRORDERING . NIL . 7 .)(|∀Q Q0.LF(Q,Q0)⊃¬EF(Q,Q0)∧¬GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.LF(Q,Q0)⊃¬EF(Q,Q0)∧¬GF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#8) . NIL . FRORDERING . NIL . 8 .)(|∀Q Q0.GF(Q,Q0)≡LF(Q0,Q)| . (AXIOM (TM& . |∀Q Q0.GF(Q,Q0)≡LF(Q0,Q)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF LF) . NIL . (FRORDERING#9) . NIL . FRORDERING . NIL . 9 .)(|∀Q Q1 Q0.EF(Q,Q1)∧LF(Q,Q0)⊃LF(Q1,Q0)| . (AXIOM (TM& . |∀Q Q1 Q0.EF(Q,Q1)∧LF(Q,Q0)⊃LF(Q1,Q0)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF) . NIL . (FRORDERING#10) . NIL . FRORDERING . NIL . 10 .)(|∀Q Q0 Q01.LF(Q,Q0)∧EF(Q0,Q01)⊃LF(Q,Q01)| . (AXIOM (TM& . |∀Q Q0 Q01.LF(Q,Q0)∧EF(Q0,Q01)⊃LF(Q,Q01)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF) . NIL . (FRORDERING#11) . NIL . FRORDERING . NIL . 11 .)(|∀Q Q1 Q0 Q01.LF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LF(Q1,Q01)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF) . NIL . (FRORDERING#12) . NIL . FRORDERING . NIL . 12 .)(|∀Q Q1 Q0 Q01.GF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.GF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GF(Q1,Q01)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF) . NIL . (FRORDERING#13) . NIL . FRORDERING . NIL . 13 .)(NIL . (DECL GEF (TYPE: (TY& . @EF))) . ((GEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#14 . NIL . VARIABLE .)) EF) . NIL . NIL . NIL . FRORDERING . NIL . 14 .)(|∀Q Q0.GEF(Q,Q0)≡EF(Q,Q0)∨GF(Q,Q0)| . (DEFINE GEF (TM& . |∀Q Q0.GEF(Q,Q0)≡EF(Q,Q0)∨GF(Q,Q0)|) NIL) . ((GEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#15 . NIL . DEFINED .)) M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF) . NIL . (FRORDERING#15 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9) . NIL . FRORDERING . NIL . 15 .)(NIL . (DECL LEF (TYPE: (TY& . @EF))) . ((LEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#16 . NIL . VARIABLE .)) EF) . NIL . NIL . NIL . FRORDERING . NIL . 16 .)(|∀Q Q0.LEF(Q,Q0)≡EF(Q,Q0)∨LF(Q,Q0)| . (DEFINE LEF (TM& . |∀Q Q0.LEF(Q,Q0)≡EF(Q,Q0)∨LF(Q,Q0)|) NIL) . ((LEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#17 . NIL . DEFINED .)) M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF) . NIL . (FRORDERING#17 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9) . NIL . FRORDERING . NIL . 17 .)(|∀Q Q1 Q0 Q01.GEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GEF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.GEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GEF(Q1,Q01)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF GEF) . NIL . (FRORDERING#18) . NIL . FRORDERING . NIL . 18 .)(|∀Q Q1 Q0 Q01.LEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LEF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LEF(Q1,Q01)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#19) . NIL . FRORDERING . NIL . 19 .)(|∀Q Q0.GEF(Q,Q0)≡LEF(Q0,Q)| . (AXIOM (TM& . |∀Q Q0.GEF(Q,Q0)≡LEF(Q0,Q)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF GEF LEF) . NIL . (FRORDERING#20) . NIL . FRORDERING . NIL . 20 .)(|∀Q1 Q2 Q3.LF(Q1,Q2)∧LF(Q2,Q3)⊃LF(Q1,Q3)| . (AXIOM (TM& . |∀Q1 Q2 Q3.LF(Q1,Q2)∧LF(Q2,Q3)⊃LF(Q1,Q3)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF) . NIL . (FRORDERING#21) . NIL . FRORDERING . NIL . 21 .)(|∀Q Q1 Q2.LEF(Q,Q1)∧LF(Q1,Q2)⊃LF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.LEF(Q,Q1)∧LF(Q1,Q2)⊃LF(Q,Q2)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#22) . NIL . FRORDERING . NIL . 22 .)(|∀Q Q1 Q2.LF(Q,Q1)∧LEF(Q1,Q2)⊃LF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.LF(Q,Q1)∧LEF(Q1,Q2)⊃LF(Q,Q2)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#23) . NIL . FRORDERING . NIL . 23 .)(|∀Q Q1 Q2.LEF(Q,Q1)∧LEF(Q1,Q2)⊃LEF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.LEF(Q,Q1)∧LEF(Q1,Q2)⊃LEF(Q,Q2)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#24) . NIL . FRORDERING . NIL . 24 .)(|∀Q.(∃Q0.GF(Q0,Q))| . (AXIOM (TM& . |∀Q.(∃Q0.GF(Q0,Q))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF) . NIL . (FRORDERING#25) . NIL . FRORDERING . NIL . 25 .)(|∀Q.(∃Q0.LF(Q0,Q))| . (AXIOM (TM& . |∀Q.(∃Q0.LF(Q0,Q))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF) . NIL . (FRORDERING#26) . NIL . FRORDERING . NIL . 26 .)(|∀Q Q1.(∃Q0.LF(Q,Q1)⊃LF(Q,Q0)∧LF(Q0,Q1))| . (AXIOM (TM& . |∀Q Q1.(∃Q0.LF(Q,Q1)⊃LF(Q,Q0)∧LF(Q0,Q1))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF) . NIL . (FRORDERING#27) . NIL . FRORDERING . NIL . 27 .)(|QZ=LIST(0,1)| . (DEFINE QZ (TM& . |QZ=LIST(0,1)|) NIL) . ((QZ . (GROUND . (SYMBOL& FR NIL) . NIL . ((BINDP& . 1000)) . FRORDERING#28 . NIL . DEFINED .)) LIST FR) . NIL . (FRORDERING#28 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9) . NIL . FRORDERING . NIL . 28 .)(|FR(QZ)| . (AXIOM (TM& . |FR(QZ)|)) . (LIST FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QZ) . NIL . (FRORDERING#29) . NIL . FRORDERING . NIL . 29 .)(|QZEROP=(λQ.EF(Q,QZ))| . (DEFINE QZEROP (TM& . |QZEROP=(λQ.EF(Q,QZ))|) NIL) . ((QZEROP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#30 . NIL . DEFINED .)) M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ) . NIL . (FRORDERING#30 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29) . NIL . FRORDERING . NIL . 30 .)(|∀Q.LEF(QZ,Q)| . (AXIOM (TM& . |∀Q.LEF(QZ,Q)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF QZ) . NIL . (FRORDERING#31) . NIL . FRORDERING . NIL . 31 .)(|QONE=LIST(1,1)| . (DEFINE QONE (TM& . |QONE=LIST(1,1)|) NIL) . ((QONE . (GROUND . (SYMBOL& FR NIL) . NIL . ((BINDP& . 1000)) . FRORDERING#32 . NIL . DEFINED .)) LIST FR) . NIL . (FRORDERING#32 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31) . NIL . FRORDERING . NIL . 32 .)(|FR(QONE)| . (AXIOM (TM& . |FR(QONE)|)) . (LIST FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QONE) . NIL . (FRORDERING#33) . NIL . FRORDERING . NIL . 33 .)(|PF=(λQ Q0.LIST(CAR Q*CADR(Q0)+CADR(Q)*CAR Q0,CADR(Q)*CADR(Q0)))| . (DEFINE PF (TM& . |PF=(λQ Q0.LIST(CAR Q*CADR(Q0)+CADR(Q)*CAR Q0,CADR(Q)*CADR(Q0)))|) NIL) . ((PF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940)) . FRACTSUM#2 . NIL . DEFINED .)) M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTSUM#2 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33) . NIL . FRACTSUM . NIL . 2 .)(|∀Q Q0.FR(PF(Q,Q0))| . (AXIOM (TM& . |∀Q Q0.FR(PF(Q,Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q PF) . NIL . (FRACTSUM#3) . NIL . FRACTSUM . NIL . 3 .)(|∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(PF(Q,Q0),PF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(PF(Q,Q0),PF(Q1,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#4) . NIL . FRACTSUM . NIL . 4 .)(|∀Q Q0.CADR(Q)=CADR(Q0)⊃EF(PF(Q,Q0),LIST(CAR Q+CAR Q0,CADR(Q)))| . (AXIOM (TM& . |∀Q Q0.CADR(Q)=CADR(Q0)⊃EF(PF(Q,Q0),LIST(CAR Q+CAR Q0,CADR(Q)))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#5) . NIL . FRACTSUM . NIL . 5 .)(|∀Q Q0.EF(PF(Q,Q0),PF(Q0,Q))| . (AXIOM (TM& . |∀Q Q0.EF(PF(Q,Q0),PF(Q0,Q))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#6) . NIL . FRACTSUM . NIL . 6 .)(|∀Q Q0 Q01.PF(PF(Q,Q0),Q01)=PF(Q,PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.PF(PF(Q,Q0),Q01)=PF(Q,PF(Q0,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q PF) . NIL . (FRACTSUM#7) . NIL . FRACTSUM . NIL . 7 .)(|∀Q Q0.¬EF(Q0,QZ)⊃LF(Q,PF(Q,Q0))| . (AXIOM (TM& . |∀Q Q0.¬EF(Q0,QZ)⊃LF(Q,PF(Q,Q0))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF QZ PF) . NIL . (FRACTSUM#8) . NIL . FRACTSUM . NIL . 8 .)(|∀Q Q0 Q01.LF(Q,Q0)⊃LF(PF(Q,Q01),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.LF(Q,Q0)⊃LF(PF(Q,Q01),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF PF) . NIL . (FRACTSUM#9) . NIL . FRACTSUM . NIL . 9 .)(|∀Q Q0 Q01.EF(Q,Q0)⊃EF(PF(Q,Q01),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.EF(Q,Q0)⊃EF(PF(Q,Q01),PF(Q0,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#10) . NIL . FRACTSUM . NIL . 10 .)(|∀Q Q0 Q01.GF(Q,Q0)⊃GF(PF(Q,Q01),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.GF(Q,Q0)⊃GF(PF(Q,Q01),PF(Q0,Q01))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF PF) . NIL . (FRACTSUM#11) . NIL . FRACTSUM . NIL . 11 .)(|∀Q Q0 Q01.GF(PF(Q,Q01),PF(Q0,Q01))⊃GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.GF(PF(Q,Q01),PF(Q0,Q01))⊃GF(Q,Q0)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF PF) . NIL . (FRACTSUM#12) . NIL . FRACTSUM . NIL . 12 .)(|∀Q Q0 Q01.EF(PF(Q,Q01),PF(Q0,Q01))⊃EF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.EF(PF(Q,Q01),PF(Q0,Q01))⊃EF(Q,Q0)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#13) . NIL . FRACTSUM . NIL . 13 .)(|∀Q Q0 Q01.LF(PF(Q,Q01),PF(Q0,Q01))⊃LF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.LF(PF(Q,Q01),PF(Q0,Q01))⊃LF(Q,Q0)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF PF) . NIL . (FRACTSUM#14) . NIL . FRACTSUM . NIL . 14 .)(|∀Q Q0 Q1 Q01.GF(Q,Q0)∧GF(Q1,Q01)⊃GF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.GF(Q,Q0)∧GF(Q1,Q01)⊃GF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF PF) . NIL . (FRACTSUM#15) . NIL . FRACTSUM . NIL . 15 .)(|∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF PF) . NIL . (FRACTSUM#16) . NIL . FRACTSUM . NIL . 16 .)(|∀Q Q0 Q1 Q01.LF(Q,Q0)∧LEF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.LF(Q,Q0)∧LEF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF PF) . NIL . (FRACTSUM#17) . NIL . FRACTSUM . NIL . 17 .)(|∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LEF(Q1,Q01)⊃LEF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LEF(Q1,Q01)⊃LEF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF PF) . NIL . (FRACTSUM#18) . NIL . FRACTSUM . NIL . 18 .)(|∀Q.EF(PF(Q,QZ),Q)∧EF(PF(QZ,Q),Q)| . (AXIOM (TM& . |∀Q.EF(PF(Q,QZ),Q)∧EF(PF(QZ,Q),Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ PF) . NIL . (FRACTSUM#19) . NIL . FRACTSUM . NIL . 19 .)(|∀Q0 Q.(∃Q1.LF(Q,Q0)⊃EF(PF(Q,Q1),Q0))| . (AXIOM (TM& . |∀Q0 Q.(∃Q1.LF(Q,Q0)⊃EF(PF(Q,Q1),Q0))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF PF) . NIL . (FRACTSUM#20) . NIL . FRACTSUM . NIL . 20 .)(|∀Q0 Q.LF(Q,Q0)⊃EF(PF(Q,MINUS(Q0,Q)),Q0)| . (DEFINE MINUS (TM& . |∀Q0 Q.LF(Q,Q0)⊃EF(PF(Q,MINUS(Q0,Q)),Q0)|) ((USE (LR& FRACTSUM#20)) (USE (LR& SETS#9)))) . ((MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTSUM#21 . NIL . DEFINED .)) M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF PF) . NIL . (FRACTSUM#21 MULTIP#10 LISPAX#30 FRACTSUM#20 SETS#9 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19) . NIL . FRACTSUM . NIL . 21 .)(|TF=(λQ Q0.LIST(CAR Q*CAR Q0,CADR(Q)*CADR(Q0)))| . (DEFINE TF (TM& . |TF=(λQ Q0.LIST(CAR Q*CAR Q0,CADR(Q)*CADR(Q0)))|) NIL) . ((TF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 935)) . FRACTMULT#2 . NIL . DEFINED .)) M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTMULT#2 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19) . NIL . FRACTMULT . NIL . 2 .)(|∀Q Q0.FR(TF(Q,Q0))| . (AXIOM (TM& . |∀Q Q0.FR(TF(Q,Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q TF) . NIL . (FRACTMULT#3) . NIL . FRACTMULT . NIL . 3 .)(|∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#4) . NIL . FRACTMULT . NIL . 4 .)(|∀Q Q0.EF(TF(Q,Q0),TF(Q0,Q))| . (AXIOM (TM& . |∀Q Q0.EF(TF(Q,Q0),TF(Q0,Q))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#5) . NIL . FRACTMULT . NIL . 5 .)(|∀Q Q0 Q01.TF(TF(Q,Q0),Q01)=TF(Q,TF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.TF(TF(Q,Q0),Q01)=TF(Q,TF(Q0,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q TF) . NIL . (FRACTMULT#6) . NIL . FRACTMULT . NIL . 6 .)(|∀Q Q0 Q01.TF(Q,PF(Q0,Q01))=PF(TF(Q,Q0),TF(Q,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.TF(Q,PF(Q0,Q01))=PF(TF(Q,Q0),TF(Q,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q PF TF) . NIL . (FRACTMULT#7) . NIL . FRACTMULT . NIL . 7 .)(|∀Q Q1 Q0.GF(Q,Q1)⊃GF(TF(Q,Q0),TF(Q1,Q0))| . (AXIOM (TM& . |∀Q Q1 Q0.GF(Q,Q1)⊃GF(TF(Q,Q0),TF(Q1,Q0))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF TF) . NIL . (FRACTMULT#8) . NIL . FRACTMULT . NIL . 8 .)(|∀Q Q1 Q0.EF(Q,Q1)⊃EF(TF(Q,Q0),TF(Q1,Q0))| . (AXIOM (TM& . |∀Q Q1 Q0.EF(Q,Q1)⊃EF(TF(Q,Q0),TF(Q1,Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#9) . NIL . FRACTMULT . NIL . 9 .)(|∀Q Q1 Q0.LF(Q,Q1)⊃LF(TF(Q,Q0),TF(Q1,Q0))| . (AXIOM (TM& . |∀Q Q1 Q0.LF(Q,Q1)⊃LF(TF(Q,Q0),TF(Q1,Q0))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF TF) . NIL . (FRACTMULT#10) . NIL . FRACTMULT . NIL . 10 .)(|∀Q Q0 Q01.GF(TF(Q,Q01),TF(Q0,Q01))⊃GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.GF(TF(Q,Q01),TF(Q0,Q01))⊃GF(Q,Q0)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF TF) . NIL . (FRACTMULT#11) . NIL . FRACTMULT . NIL . 11 .)(|∀Q Q0 Q01.EF(TF(Q,Q01),TF(Q0,Q01))⊃EF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.EF(TF(Q,Q01),TF(Q0,Q01))⊃EF(Q,Q0)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#12) . NIL . FRACTMULT . NIL . 12 .)(|∀Q Q0 Q01.LF(TF(Q,Q01),TF(Q0,Q01))⊃LF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.LF(TF(Q,Q01),TF(Q0,Q01))⊃LF(Q,Q0)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF TF) . NIL . (FRACTMULT#13) . NIL . FRACTMULT . NIL . 13 .)(|∀Q Q1 Q0 Q01.GF(Q,Q1)∧GF(Q0,Q01)⊃GF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.GF(Q,Q1)∧GF(Q0,Q01)⊃GF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF TF) . NIL . (FRACTMULT#14) . NIL . FRACTMULT . NIL . 14 .)(|∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF TF) . NIL . (FRACTMULT#15) . NIL . FRACTMULT . NIL . 15 .)(|∀Q Q1 Q0 Q01.LF(Q,Q1)∧LEF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LF(Q,Q1)∧LEF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF TF) . NIL . (FRACTMULT#16) . NIL . FRACTMULT . NIL . 16 .)(|∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LEF(Q0,Q01)⊃LEF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LEF(Q0,Q01)⊃LEF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF TF) . NIL . (FRACTMULT#17) . NIL . FRACTMULT . NIL . 17 .)(|INV=(λQ.LIST(CADR(Q),CAR Q))| . (DEFINE INV (TM& . |INV=(λQ.LIST(CADR(Q),CAR Q))|) NIL) . ((INV . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTMULT#18 . NIL . DEFINED .)) CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTMULT#18 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3) . NIL . FRACTMULT . NIL . 18 .)(|∀Q.¬QZEROP(Q)⊃FR(INV(Q))| . (AXIOM (TM& . |∀Q.¬QZEROP(Q)⊃FR(INV(Q))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP INV) . NIL . (FRACTMULT#19) . NIL . FRACTMULT . NIL . 19 .)(|∀Q.TF(Q,QONE)=Q| . (AXIOM (TM& . |∀Q.TF(Q,QONE)=Q|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QONE TF) . NIL . (FRACTMULT#20) . NIL . FRACTMULT . NIL . 20 .)(|∀Q.TF(QONE,Q)=Q| . (AXIOM (TM& . |∀Q.TF(QONE,Q)=Q|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QONE TF) . NIL . (FRACTMULT#21) . NIL . FRACTMULT . NIL . 21 .)(|∀Q.¬QZEROP(Q)⊃EF(TF(Q,INV(Q)),QONE)| . (AXIOM (TM& . |∀Q.¬QZEROP(Q)⊃EF(TF(Q,INV(Q)),QONE)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP QONE TF INV) . NIL . (FRACTMULT#22) . NIL . FRACTMULT . NIL . 22 .)(|∀Q.EF(TF(Q,QZ),QZ)| . (AXIOM (TM& . |∀Q.EF(TF(Q,QZ),QZ)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ TF) . NIL . (FRACTMULT#23) . NIL . FRACTMULT . NIL . 23 .)(|∀Q0 Q.(∃Q1.¬QZEROP(Q)⊃EF(TF(Q,Q1),Q0))| . (AXIOM (TM& . |∀Q0 Q.(∃Q1.¬QZEROP(Q)⊃EF(TF(Q,Q1),Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP TF) . NIL . (FRACTMULT#24) . NIL . FRACTMULT . NIL . 24 .)(|∀Q Q0.¬QZEROP(Q)⊃EF(TF(Q,DIVIDED(Q0,Q)),Q0)| . (DEFINE DIVIDED (TM& . |∀Q Q0.¬QZEROP(Q)⊃EF(TF(Q,DIVIDED(Q0,Q)),Q0)|) ((USE (LR& FRACTMULT#24)) (USE (LR& SETS#9)))) . ((DIVIDED . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTMULT#25 . NIL . DEFINED .)) M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP TF) . NIL . (FRACTMULT#25 MULTIP#10 LISPAX#30 FRACTMULT#24 SETS#9 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19) . NIL . FRACTMULT . NIL . 25 .)(|∀Q.EQCLASS(Q)=(λQ0.EF(Q0,Q))| . (DEFINE EQCLASS (TM& . |∀Q.EQCLASS(Q)=(λQ0.EF(Q0,Q))|) NIL) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF R (EQCLASS . (|(@Q)→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . RATIONAL#4 . NIL . DEFINED .))) . NIL . (RATIONAL#4 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19) . NIL . RATIONAL . NIL . 4 .)(|∀Q.RATIO(EQCLASS(Q))| . (AXIOM (TM& . |∀Q.RATIO(EQCLASS(Q))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS) . NIL . (RATIONAL#5) . NIL . RATIONAL . NIL . 5 .)(|∀R.(∃Q.R=EQCLASS(Q))| . (AXIOM (TM& . |∀R.(∃Q.R=EQCLASS(Q))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS) . NIL . (RATIONAL#6) . NIL . RATIONAL . NIL . 6 .)(NIL . (DECL REPRESENT (TYPE: (TY& . |(@R)→(@Q)|))) . ((REPRESENT . (|(@R)→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . RATIONAL#7 . NIL . VARIABLE .)) Q R) . NIL . NIL . NIL . RATIONAL . NIL . 7 .)(|∀R.EQCLASS(REPRESENT(R))=R| . (DEFINE REPRESENT (TM& . |∀R.EQCLASS(REPRESENT(R))=R|) ((USE (LR& RATIONAL#6)) (USE (LR& SETS#9)))) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS (REPRESENT . (|(@R)→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . RATIONAL#8 . NIL . DEFINED .))) . NIL . (RATIONAL#8 MULTIP#10 LISPAX#30 RATIONAL#6 SETS#9 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5) . NIL . RATIONAL . NIL . 8 .)(|∀R.FR(REPRESENT(R))| . (AXIOM (TM& . |∀R.FR(REPRESENT(R))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT) . NIL . (RATIONAL#9) . NIL . RATIONAL . NIL . 9 .)(|∀R.R(REPRESENT(R))| . (AXIOM (TM& . |∀R.R(REPRESENT(R))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT) . NIL . (RATIONAL#10) . NIL . RATIONAL . NIL . 10 .)(|∀Q.EF(REPRESENT(EQCLASS(Q)),Q)| . (AXIOM (TM& . |∀Q.EF(REPRESENT(EQCLASS(Q)),Q)|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT) . NIL . (RATIONAL#11) . NIL . RATIONAL . NIL . 11 .)(|∀R R1.EF(REPRESENT(R),REPRESENT(R1))≡R=R1| . (AXIOM (TM& . |∀R R1.EF(REPRESENT(R),REPRESENT(R1))≡R=R1|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT) . NIL . (RATIONAL#12) . NIL . RATIONAL . NIL . 12 .)(|∀Q Q0.EF(Q,Q0)≡EQCLASS(Q)=EQCLASS(Q0)| . (AXIOM (TM& . |∀Q Q0.EF(Q,Q0)≡EQCLASS(Q)=EQCLASS(Q0)|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF R EQCLASS) . NIL . (RATIONAL#13) . NIL . RATIONAL . NIL . 13 .)(|∀R R0.R ++ R0=EQCLASS(PF(REPRESENT(R),REPRESENT(R0)))| . (DEFAX ADDRAT (TM& . |∀R R0.R ++ R0=EQCLASS(PF(REPRESENT(R),REPRESENT(R0)))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT (ADDRAT . (|((@R)*)→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 948) (INFIX& . ++)) . ADDRAT#2 . NIL . DEFINED .))) . NIL . (ADDRAT#2) . NIL . ADDRAT . NIL . 2 .)(|∀R R0.R ** R0=EQCLASS(TF(REPRESENT(R),REPRESENT(R0)))| . (DEFAX MULTRAT (TM& . |∀R R0.R ** R0=EQCLASS(TF(REPRESENT(R),REPRESENT(R0)))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT (MULTRAT . (|((@R)*)→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 949) (INFIX& . **)) . MULTRAT#2 . NIL . DEFINED .))) . NIL . (MULTRAT#2) . NIL . MULTRAT . NIL . 2 .)(|∀R R1.R >> R1=GF(REPRESENT(R),REPRESENT(R1))| . (DEFINE GREATRAT (TM& . |∀R R1.R >> R1=GF(REPRESENT(R),REPRESENT(R1))|) NIL) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT (GREATRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . >>)) . ORDRAT#2 . NIL . DEFINED .))) . NIL . (ORDRAT#2 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10) . NIL . ORDRAT . NIL . 2 .)(NIL . (DECL LESSRAT (TYPE: (TY& . |((@R)⊗(@R))→TRUTHVAL|)) (INFIXNAME: <<) (SYNTYPE: CONSTANT) (BINDINGPOWER: 945)) . ((LESSRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . <<)) . ORDRAT#3 . NIL . CONSTANT .)) R) . NIL . NIL . NIL . ORDRAT . NIL . 3 .)(|∀R R1.R << R1=LF(REPRESENT(R),REPRESENT(R1))| . (DEFINE LESSRAT (TM& . |∀R R1.R << R1=LF(REPRESENT(R),REPRESENT(R1))|) NIL) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT (LESSRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . <<)) . ORDRAT#4 . NIL . DEFINED .))) . NIL . (ORDRAT#4 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10) . NIL . ORDRAT . NIL . 4 .)(|∀R R0.RATIO(R ++ R0)| . (AXIOM (TM& . |∀R R0.RATIO(R ++ R0)|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT) . NIL . (ADDRAT#3) . NIL . ADDRAT . NIL . 3 .)(|∀R R1.EF(REPRESENT(R ++ R1),PF(REPRESENT(R),REPRESENT(R1)))| . (AXIOM (TM& . |∀R R1.EF(REPRESENT(R ++ R1),PF(REPRESENT(R),REPRESENT(R1)))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT) . NIL . (ADDRAT#4) . NIL . ADDRAT . NIL . 4 .)(|∀Q Q1.EQCLASS(Q) ++ EQCLASS(Q1)=EQCLASS(PF(Q,Q1))| . (AXIOM (TM& . |∀Q Q1.EQCLASS(Q) ++ EQCLASS(Q1)=EQCLASS(PF(Q,Q1))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT) . NIL . (ADDRAT#5) . NIL . ADDRAT . NIL . 5 .)(|∀R R0.R ++ R0=R0 ++ R| . (AXIOM (TM& . |∀R R0.R ++ R0=R0 ++ R|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT) . NIL . (ADDRAT#6) . NIL . ADDRAT . NIL . 6 .)(|∀R R0 R1.(R ++ R0) ++ R1=R ++ (R0 ++ R1)| . (AXIOM (TM& . |∀R R0 R1.(R ++ R0) ++ R1=R ++ (R0 ++ R1)|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT) . NIL . (ADDRAT#7) . NIL . ADDRAT . NIL . 7 .)(|∀R R1.RATIO(R ** R1)| . (AXIOM (TM& . |∀R R1.RATIO(R ** R1)|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT MULTRAT) . NIL . (MULTRAT#3) . NIL . MULTRAT . NIL . 3 .)(|∀R R1.EF(REPRESENT(R ** R1),TF(REPRESENT(R),REPRESENT(R1)))| . (AXIOM (TM& . |∀R R1.EF(REPRESENT(R ** R1),TF(REPRESENT(R),REPRESENT(R1)))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT MULTRAT) . NIL . (MULTRAT#4) . NIL . MULTRAT . NIL . 4 .)(|∀Q Q1.EQCLASS(Q) ** EQCLASS(Q1)=EQCLASS(TF(Q,Q1))| . (AXIOM (TM& . |∀Q Q1.EQCLASS(Q) ** EQCLASS(Q1)=EQCLASS(TF(Q,Q1))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT MULTRAT) . NIL . (MULTRAT#5) . NIL . MULTRAT . NIL . 5 .)(|∀R R1.R ** R1=R1 ** R| . (AXIOM (TM& . |∀R R1.R ** R1=R1 ** R|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT MULTRAT) . NIL . (MULTRAT#6) . NIL . MULTRAT . NIL . 6 .)(|∀R R1 R2.(R ** R1) ** R2=R ** (R1 ** R2)| . (AXIOM (TM& . |∀R R1 R2.(R ** R1) ** R2=R ** (R1 ** R2)|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT MULTRAT) . NIL . (MULTRAT#7) . NIL . MULTRAT . NIL . 7 .)(|∀R0 R1 R2.R0 ** (R1 ++ R2)=R0 ** R1 ++ R0 ** R2| . (AXIOM (TM& . |∀R0 R1 R2.R0 ** (R1 ++ R2)=R0 ** R1 ++ R0 ** R2|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT MULTRAT) . NIL . (MULTRAT#8) . NIL . MULTRAT . NIL . 8 .)(|∀R R1.R << R1∨R=R1∨R >> R1| . (AXIOM (TM& . |∀R R1.R << R1∨R=R1∨R >> R1|)) . (M N K J I ADD1 LESSP GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT LESSRAT) . NIL . (ORDRAT#5) . NIL . ORDRAT . NIL . 5 .)(|∀R R1.R=R1⊃¬R << R1∧¬R >> R1| . (AXIOM (TM& . |∀R R1.R=R1⊃¬R << R1∧¬R >> R1|)) . (M N K J I ADD1 LESSP GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT LESSRAT) . NIL . (ORDRAT#6) . NIL . ORDRAT . NIL . 6 .)(|∀R R1.R >> R1⊃¬R=R1∧¬R << R1| . (AXIOM (TM& . |∀R R1.R >> R1⊃¬R=R1∧¬R << R1|)) . (M N K J I ADD1 LESSP GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT LESSRAT) . NIL . (ORDRAT#7) . NIL . ORDRAT . NIL . 7 .)(|∀R R1.R << R1⊃¬R=R1∧¬R >> R1| . (AXIOM (TM& . |∀R R1.R << R1⊃¬R=R1∧¬R >> R1|)) . (M N K J I ADD1 LESSP GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT LESSRAT) . NIL . (ORDRAT#8) . NIL . ORDRAT . NIL . 8 .)(|∀R R0.R << R0⊃¬R=R0| . (AXIOM (TM& . |∀R R0.R << R0⊃¬R=R0|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT) . NIL . (ORDRAT#9) . NIL . ORDRAT . NIL . 9 .)(|∀R R1.R >> R1≡R1 << R| . (AXIOM (TM& . |∀R R1.R >> R1≡R1 << R|)) . (M N K J I ADD1 LESSP GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT LESSRAT) . NIL . (ORDRAT#10) . NIL . ORDRAT . NIL . 10 .)(|∀R R0.R << R0⊃¬R0 << R| . (AXIOM (TM& . |∀R R0.R << R0⊃¬R0 << R|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT) . NIL . (ORDRAT#11) . NIL . ORDRAT . NIL . 11 .)(NIL . (DECL GEQRAT (TYPE: (TY& . |((@R)⊗(@R))→TRUTHVAL|)) (INFIXNAME: >=) (SYNTYPE: CONSTANT) (BINDINGPOWER: 945)) . ((GEQRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . >=)) . ORDRAT#12 . NIL . CONSTANT .)) R) . NIL . NIL . NIL . ORDRAT . NIL . 12 .)(|∀R R1.R >= R1≡R=R1∨R >> R1| . (DEFINE GEQRAT (TM& . |∀R R1.R >= R1≡R=R1∨R >> R1|) NIL) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT (GEQRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . >=)) . ORDRAT#13 . NIL . DEFINED .))) . NIL . (ORDRAT#13 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11) . NIL . ORDRAT . NIL . 13 .)(NIL . (DECL LEQRAT (TYPE: (TY& . |((@R)⊗(@R))→TRUTHVAL|)) (INFIXNAME: =<) (SYNTYPE: CONSTANT) (BINDINGPOWER: 945)) . ((LEQRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . =<)) . ORDRAT#14 . NIL . CONSTANT .)) R) . NIL . NIL . NIL . ORDRAT . NIL . 14 .)(|∀R R1.R =< R1≡R=R1∨R << R1| . (DEFINE LEQRAT (TM& . |∀R R1.R =< R1≡R=R1∨R << R1|) NIL) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT (LEQRAT . (|((@R)⊗(@R))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 945) (INFIX& . =<)) . ORDRAT#15 . NIL . DEFINED .))) . NIL . (ORDRAT#15 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11) . NIL . ORDRAT . NIL . 15 .)(|∀R R1.R =< R1≡LEF(REPRESENT(R),REPRESENT(R1))| . (AXIOM (TM& . |∀R R1.R =< R1≡LEF(REPRESENT(R),REPRESENT(R1))|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF LEF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT) . NIL . (ORDRAT#16) . NIL . ORDRAT . NIL . 16 .)(|∀R R1.R >= R1≡GEF(REPRESENT(R),REPRESENT(R1))| . (AXIOM (TM& . |∀R R1.R >= R1≡GEF(REPRESENT(R),REPRESENT(R1))|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF GEF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT GEQRAT) . NIL . (ORDRAT#17) . NIL . ORDRAT . NIL . 17 .)(|∀R R1.R >= R1≡R1 =< R| . (AXIOM (TM& . |∀R R1.R >= R1≡R1 =< R|)) . (M N K J I ADD1 LESSP GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT LESSRAT GEQRAT LEQRAT) . NIL . (ORDRAT#18) . NIL . ORDRAT . NIL . 18 .)(|∀R R1 R2.R << R1∧R1 << R2⊃R << R2| . (AXIOM (TM& . |∀R R1 R2.R << R1∧R1 << R2⊃R << R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT) . NIL . (ORDRAT#19) . NIL . ORDRAT . NIL . 19 .)(|∀R R1 R2.R =< R1∧R1 << R2⊃R << R2| . (AXIOM (TM& . |∀R R1 R2.R =< R1∧R1 << R2⊃R << R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT) . NIL . (ORDRAT#20) . NIL . ORDRAT . NIL . 20 .)(|∀R R1 R2.R << R1∧R1 =< R2⊃R << R2| . (AXIOM (TM& . |∀R R1 R2.R << R1∧R1 =< R2⊃R << R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT) . NIL . (ORDRAT#21) . NIL . ORDRAT . NIL . 21 .)(|∀R R1 R2.R =< R1∧R1 =< R2⊃R =< R2| . (AXIOM (TM& . |∀R R1 R2.R =< R1∧R1 =< R2⊃R =< R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT) . NIL . (ORDRAT#22) . NIL . ORDRAT . NIL . 22 .)(|∀R.(∃R1.R1 >> R)| . (AXIOM (TM& . |∀R.(∃R1.R1 >> R)|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT) . NIL . (ORDRAT#23) . NIL . ORDRAT . NIL . 23 .)(|∀R.(∃R0.R0 << R)| . (AXIOM (TM& . |∀R.(∃R0.R0 << R)|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT) . NIL . (ORDRAT#24) . NIL . ORDRAT . NIL . 24 .)(|∀R R1.(∃R0.R << R1⊃R << R0∧R0 << R1)| . (AXIOM (TM& . |∀R R1.(∃R0.R << R1⊃R << R0∧R0 << R1)|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT) . NIL . (ORDRAT#25) . NIL . ORDRAT . NIL . 25 .)(|QZERO=EQCLASS()| . (DEFINE QZERO (TM& . |QZERO=EQCLASS()|) NIL) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF R EQCLASS (|| . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ORDRAT#26 . NIL . VARIABLE .)) (QZERO . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ORDRAT#26 . NIL . DEFINED .))) . NIL . (ORDRAT#26 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11) . NIL . ORDRAT . NIL . 26 .)(NIL . (DECL RZEROP (TYPE: (TY& . |(@R)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((RZEROP . (|(@R)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ORDRAT#27 . NIL . CONSTANT .)) R) . NIL . NIL . NIL . ORDRAT . NIL . 27 .)(|RZEROP=(λR.REPRESENT(R)=QZ)| . (DEFINE RZEROP (TM& . |RZEROP=(λR.REPRESENT(R)=QZ)|) NIL) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF QZ RATIO R2 R1 R0 R EQCLASS REPRESENT (RZEROP . (|(@R)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ORDRAT#28 . NIL . DEFINED .))) . NIL . (ORDRAT#28 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11) . NIL . ORDRAT . NIL . 28 .)(|RONE=EQCLASS(QONE)| . (DEFINE RONE (TM& . |RONE=EQCLASS(QONE)|) NIL) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF QONE RATIO R EQCLASS (RONE . (|(@Q)→TRUTHVAL| . (SYMBOL& RATIO NIL) . NIL . ((BINDP& . 1000)) . ORDRAT#29 . NIL . DEFINED .))) . NIL . (ORDRAT#29 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11) . NIL . ORDRAT . NIL . 29 .)(NIL . (DECL RONEP (TYPE: (TY& . |(@R)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((RONEP . (|(@R)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ORDRAT#30 . NIL . CONSTANT .)) R) . NIL . NIL . NIL . ORDRAT . NIL . 30 .)(|RONEP=(λR.REPRESENT(R)=QONE)| . (DEFINE RONEP (TM& . |RONEP=(λR.REPRESENT(R)=QONE)|) NIL) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF QONE RATIO R2 R1 R0 R EQCLASS REPRESENT (RONEP . (|(@R)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ORDRAT#31 . NIL . DEFINED .))) . NIL . (ORDRAT#31 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11) . NIL . ORDRAT . NIL . 31 .)(|∀R R0.RZEROP(R0)⊃¬R << R0| . (AXIOM (TM& . |∀R R0.RZEROP(R0)⊃¬R << R0|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF LF QZ RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT RZEROP) . NIL . (ORDRAT#32) . NIL . ORDRAT . NIL . 32 .)(|∀R.RZERO =< R| . (AXIOM (TM& . |∀R.RZERO =< R|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT (RZERO . (|(@Q)→TRUTHVAL| . (SYMBOL& RATIO NIL) . NIL . ((BINDP& . 1000)) . ORDRAT#33 . NIL . VARIABLE .))) . NIL . (ORDRAT#33) . NIL . ORDRAT . NIL . 33 .)(|∀R R1.¬RZEROP(R1)⊃R ++ R1 >> R| . (AXIOM (TM& . |∀R R1.¬RZEROP(R1)⊃R ++ R1 >> R|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PF PLUS LIST XV CADR EF QZ RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT RZEROP ADDRAT) . NIL . (ADDRAT#8) . NIL . ADDRAT . NIL . 8 .)(|∀R R0 R1.R >> R0⊃R ++ R1 >> R0 ++ R1| . (AXIOM (TM& . |∀R R0 R1.R >> R0⊃R ++ R1 >> R0 ++ R1|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT ADDRAT) . NIL . (ADDRAT#9) . NIL . ADDRAT . NIL . 9 .)(|∀R R0 R1.R=R0⊃R ++ R1=R0 ++ R1| . (AXIOM (TM& . |∀R R0 R1.R=R0⊃R ++ R1=R0 ++ R1|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT) . NIL . (ADDRAT#10) . NIL . ADDRAT . NIL . 10 .)(|∀R R0 R1.R ++ R1 >> R0 ++ R1⊃R >> R0| . (AXIOM (TM& . |∀R R0 R1.R ++ R1 >> R0 ++ R1⊃R >> R0|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT ADDRAT) . NIL . (ADDRAT#11) . NIL . ADDRAT . NIL . 11 .)(|∀R R0 R1.R ++ R1=R0 ++ R1⊃R=R0| . (AXIOM (TM& . |∀R R0 R1.R ++ R1=R0 ++ R1⊃R=R0|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT ADDRAT) . NIL . (ADDRAT#12) . NIL . ADDRAT . NIL . 12 .)(|∀R R0 R1 R2.R1 >> R∧R2 >> R0⊃R1 ++ R2 >> R ++ R0| . (AXIOM (TM& . |∀R R0 R1 R2.R1 >> R∧R2 >> R0⊃R1 ++ R2 >> R ++ R0|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT ADDRAT) . NIL . (ADDRAT#13) . NIL . ADDRAT . NIL . 13 .)(|∀R R0 R1 R2.R =< R1∧R0 << R2⊃R ++ R0 << R1 ++ R2| . (AXIOM (TM& . |∀R R0 R1 R2.R =< R1∧R0 << R2⊃R ++ R0 << R1 ++ R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT ADDRAT) . NIL . (ADDRAT#14) . NIL . ADDRAT . NIL . 14 .)(|∀R R0 R1 R2.R << R1∧R0 =< R2⊃R ++ R0 << R1 ++ R2| . (AXIOM (TM& . |∀R R0 R1 R2.R << R1∧R0 =< R2⊃R ++ R0 << R1 ++ R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT ADDRAT) . NIL . (ADDRAT#15) . NIL . ADDRAT . NIL . 15 .)(|∀R R0 R1 R2.R =< R1∧R0 =< R2⊃R ++ R0 =< R1 ++ R2| . (AXIOM (TM& . |∀R R0 R1 R2.R =< R1∧R0 =< R2⊃R ++ R0 =< R1 ++ R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT ADDRAT) . NIL . (ADDRAT#16) . NIL . ADDRAT . NIL . 16 .)(|∀R R0.(∃R1.R0 =< R⊃R ++ R0=R1)| . (AXIOM (TM& . |∀R R0.(∃R1.R0 =< R⊃R ++ R0=R1)|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT ADDRAT) . NIL . (ADDRAT#17) . NIL . ADDRAT . NIL . 17 .)(|∀R R1 R2.¬RZEROP(R2)⊃R >> R1≡R ** R2 >> R1 ** R2| . (AXIOM (TM& . |∀R R1 R2.¬RZEROP(R2)⊃R >> R1≡R ** R2 >> R1 ** R2|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF TF PLUS LIST XV CADR EF QZ RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT RZEROP MULTRAT) . NIL . (MULTRAT#9) . NIL . MULTRAT . NIL . 9 .)(|∀R R1 R2.¬RZEROP(R2)⊃R ** R2=R1 ** R2≡R0=R1| . (AXIOM (TM& . |∀R R1 R2.¬RZEROP(R2)⊃R ** R2=R1 ** R2≡R0=R1|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF QZ RATIO R2 R1 R0 R EQCLASS REPRESENT RZEROP MULTRAT) . NIL . (MULTRAT#10) . NIL . MULTRAT . NIL . 10 .)(|∀R R1 R2.¬RZEROP(R2)⊃R << R1≡R ** R2 << R1 ** R2| . (AXIOM (TM& . |∀R R1 R2.¬RZEROP(R2)⊃R << R1≡R ** R2 << R1 ** R2|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF LF QZ RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT RZEROP MULTRAT) . NIL . (MULTRAT#11) . NIL . MULTRAT . NIL . 11 .)(|∀R R0 R1 R2.R >> R1∧R0 >> R2⊃R ** R0 >> R1 ** R2| . (AXIOM (TM& . |∀R R0 R1 R2.R >> R1∧R0 >> R2⊃R ** R0 >> R1 ** R2|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT MULTRAT) . NIL . (MULTRAT#12) . NIL . MULTRAT . NIL . 12 .)(|∀R R0 R1 R2.R >= R1∧R0 >> R2⊃R ** R0 >> R1 ** R2| . (AXIOM (TM& . |∀R R0 R1 R2.R >= R1∧R0 >> R2⊃R ** R0 >> R1 ** R2|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT GEQRAT MULTRAT) . NIL . (MULTRAT#13) . NIL . MULTRAT . NIL . 13 .)(|∀R R0 R1 R2.R >> R1∧R0 >= R2⊃R ** R0 >> R1 ** R2| . (AXIOM (TM& . |∀R R0 R1 R2.R >> R1∧R0 >= R2⊃R ** R0 >> R1 ** R2|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT GEQRAT MULTRAT) . NIL . (MULTRAT#14) . NIL . MULTRAT . NIL . 14 .)(|∀R R0 R1 R2.R >= R1∧R0 >= R2⊃R ** R0 >= R1 ** R2| . (AXIOM (TM& . |∀R R0 R1 R2.R >= R1∧R0 >= R2⊃R ** R0 >= R1 ** R2|)) . (M N K J I ADD1 GREATERP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF TF PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT GREATRAT GEQRAT MULTRAT) . NIL . (MULTRAT#15) . NIL . MULTRAT . NIL . 15 .)(NIL . (DECL (DIV) (TYPE: (TY& . |((@R)⊗(@R))→(@R)|)) (SYNTYPE: CONSTANT)) . ((DIV . (|((@R)⊗(@R))→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MULTRAT#16 . NIL . CONSTANT .)) R) . NIL . NIL . NIL . MULTRAT . NIL . 16 .)(|DIV=(λR R1.ERCLASS(TF(INV(REPRESENT(R1)),REPRESENT(R))))| . (DEFAX DIV (TM& . |DIV=(λR R1.ERCLASS(TF(INV(REPRESENT(R1)),REPRESENT(R))))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF INV RATIO R2 R1 R0 R EQCLASS REPRESENT (DIV . (|((@R)⊗(@R))→(@R)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MULTRAT#17 . NIL . DEFINED .)) (ERCLASS . (|GROUND→(GROUND→TRUTHVAL)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MULTRAT#17 . NIL . VARIABLE .))) . NIL . (MULTRAT#17) . NIL . MULTRAT . NIL . 17 .)(|∀Q.EQCLASS(Q) ++ RZERO=EQCLASS(Q)∧RZERO ++ EQCLASS(Q)=EQCLASS(Q)| . (AXIOM (TM& . |∀Q.EQCLASS(Q) ++ RZERO=EQCLASS(Q)∧RZERO ++ EQCLASS(Q)=EQCLASS(Q)|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT RZERO ADDRAT) . NIL . (ADDRAT#18) . NIL . ADDRAT . NIL . 18 .)(|∀R.R ++ RZERO=R∧RZERO ++ R=R| . (AXIOM (TM& . |∀R.R ++ RZERO=R∧RZERO ++ R=R|)) . (M N K J I ADD1 LESSP CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF LF RATIO R2 R1 R0 R EQCLASS REPRESENT LESSRAT LEQRAT RZERO ADDRAT) . NIL . (ADDRAT#19) . NIL . ADDRAT . NIL . 19 .)(|∀R R1.¬RZEROP(R1)⊃RATIO(DIV(R,R1))| . (AXIOM (TM& . |∀R R1.¬RZEROP(R1)⊃RATIO(DIV(R,R1))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF QZ INV RATIO R2 R1 R0 R EQCLASS REPRESENT RZEROP DIV ERCLASS) . NIL . (MULTRAT#18) . NIL . MULTRAT . NIL . 18 .)(|∀R R1.¬RZEROP(R1)⊃R1 ** DIV(R,R1)=R| . (AXIOM (TM& . |∀R R1.¬RZEROP(R1)⊃R1 ** DIV(R,R1)=R|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF QZ INV RATIO R2 R1 R0 R EQCLASS REPRESENT RZEROP MULTRAT DIV ERCLASS) . NIL . (MULTRAT#19) . NIL . MULTRAT . NIL . 19 .)(|∀R R1.¬RZEROP(R1)⊃(∃R2.R1 ** R2=R)| . (AXIOM (TM& . |∀R R1.¬RZEROP(R1)⊃(∃R2.R1 ** R2=R)|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF QZ RATIO R2 R1 R0 R EQCLASS REPRESENT RZEROP MULTRAT) . NIL . (MULTRAT#20) . NIL . MULTRAT . NIL . 20 .)(|∀R.R ** RONE=R∧RONE ** R=R| . (AXIOM (TM& . |∀R.R ** RONE=R∧RONE ** R=R|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR TF PLUS LIST XV CADR EF QONE RATIO R2 R1 R0 R EQCLASS REPRESENT RONE MULTRAT) . NIL . (MULTRAT#21) . NIL . MULTRAT . NIL . 21 .)(|∀N.INJ(N)=LIST(N,1)| . (DEFINE INJ (TM& . |∀N.INJ(N)=LIST(N,1)|) NIL) . (M N K J I LIST (INJ . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . EMBEDDING#1 . NIL . DEFINED .))) . NIL . (EMBEDDING#1 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#3 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11 ORDRAT#33 ADDRAT#3 ADDRAT#18 ADDRAT#19 MULTRAT#18 MULTIP#2 MULTIP#4 MULTIP#5 MULTIP#6 MULTIP#7 MULTIP#8 MULTIP#9 MULTIP#10 MULTIP#12 MULTIP#13) . NIL . EMBEDDING . NIL . 1 .)(|∀N.FR(INJ(N))| . (AXIOM (TM& . |∀N.FR(INJ(N))|)) . (M N K J I Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR LIST INJ) . NIL . (EMBEDDING#2) . NIL . EMBEDDING . NIL . 2 .)(|∀N M.N>M⊃GF(INJ(N),INJ(M))| . (AXIOM (TM& . |∀N M.N>M⊃GF(INJ(N),INJ(M))|)) . (M N K J I ADD1 GREATERP TIMES CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR GF PLUS LIST XV CADR INJ) . NIL . (EMBEDDING#3) . NIL . EMBEDDING . NIL . 3 .)(|∀N M.N=M⊃EF(INJ(N),INJ(M))| . (AXIOM (TM& . |∀N M.N=M⊃EF(INJ(N),INJ(M))|)) . (M N K J I ADD1 TIMES CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF INJ) . NIL . (EMBEDDING#4) . NIL . EMBEDDING . NIL . 4 .)(|∀N M.N<M⊃LF(INJ(N),INJ(M))| . (AXIOM (TM& . |∀N M.N<M⊃LF(INJ(N),INJ(M))|)) . (M N K J I ADD1 LESSP TIMES CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR LF INJ) . NIL . (EMBEDDING#5) . NIL . EMBEDDING . NIL . 5 .)(|∀R.INTEGER(R)≡(∃N.EF(REPRESENT(R),INJ(N)))| . (DEFINE INTEGER (TM& . |∀R.INTEGER(R)≡(∃N.EF(REPRESENT(R),INJ(N)))|) NIL) . (M N K J I ADD1 TIMES CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT INJ (INTEGER . (|(GROUND→TRUTHVAL)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . EMBEDDING#6 . NIL . DEFINED .))) . NIL . (EMBEDDING#6 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#3 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19 RATIONAL#5 RATIONAL#9 RATIONAL#10 ORDRAT#11 ORDRAT#33 ADDRAT#3 ADDRAT#18 ADDRAT#19 MULTRAT#18 MULTIP#2 MULTIP#4 MULTIP#5 MULTIP#6 MULTIP#7 MULTIP#8 MULTIP#9 MULTIP#10 MULTIP#12 MULTIP#13 EMBEDDING#2) . NIL . EMBEDDING . NIL . 6 .)(|∀N M.EF(PF(INJ(N),INJ(M)),INJ(N+M))| . (AXIOM (TM& . |∀N M.EF(PF(INJ(N),INJ(M)),INJ(N+M))|)) . (M N K J I ADD1 TIMES CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PF PLUS LIST XV CADR EF INJ) . NIL . (EMBEDDING#7) . NIL . EMBEDDING . NIL . 7 .)(|INTEGER(EQCLASS(INJ(0)))| . (AXIOM (TM& . |INTEGER(EQCLASS(INJ(0)))|)) . (M N K J I ADD1 TIMES CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT INJ INTEGER) . NIL . (EMBEDDING#8) . NIL . EMBEDDING . NIL . 8 .)(|∀N.INTEGER(EQCLASS(INJ(N')))| . (AXIOM (TM& . |∀N.INTEGER(EQCLASS(INJ(N')))|)) . (M N K J I ADD1 TIMES CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF RATIO R2 R1 R0 R EQCLASS REPRESENT INJ INTEGER) . NIL . (EMBEDDING#9) . NIL . EMBEDDING . NIL . 9 .)(|∀N.¬EQCLASS(INJ(N'))=EQCLASS(INJ(0))| . (AXIOM (TM& . |∀N.¬EQCLASS(INJ(N'))=EQCLASS(INJ(0))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF R EQCLASS INJ) . NIL . (EMBEDDING#10) . NIL . EMBEDDING . NIL . 10 .)(|∀N M.EQCLASS(INJ(N'))=EQCLASS(INJ(M'))≡EQCLASS(INJ(N))=EQCLASS(INJ(M))| . (AXIOM (TM& . |∀N M.EQCLASS(INJ(N'))=EQCLASS(INJ(M'))≡EQCLASS(INJ(N))=EQCLASS(INJ(M))|)) . (M N K J I ADD1 CAR CDR SEXP Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q FR PLUS LIST XV CADR EF R EQCLASS INJ) . NIL . (EMBEDDING#11) . NIL . EMBEDDING . NIL . 11 .)(|∀THETA.THETA(INJ(0))∧(∀N.THETA(INJ(N))⊃THETA(INJ(N')))⊃(∀N.THETA(INJ(N)))| . (AXIOM (TM& . |∀THETA.THETA(INJ(0))∧(∀N.THETA(INJ(N))⊃THETA(INJ(N')))⊃(∀N.THETA(INJ(N)))|)) . (M N K J I ADD1 LIST INJ (THETA . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . EMBEDDING#12 . NIL . VARIABLE .))) . NIL . (EMBEDDING#12) . NIL . EMBEDDING . NIL . 12 .)